# Quest 5 - Dependent Paths

## Part 0 - A motivating example

In Quest 0 - Working with the Circle we define the circle,
which we work with here.
We recommend also going through the definitions
for `doubleCover`

, `flipPath`

and `Flip`

in the same quest.
They will be referred to here.

```
data S¹ : Type where
base : S¹
loop : base ≡ base
```

In said quest we experience mapping out of `S¹`

by casing on
a point `x : S¹`

; this was `doubleCover`

,
it was *not a dependent function*,
in the sense that `doubleCover : (x : S¹) → Type`

where `Type`

does *not* depend on `x`

.
We give an example of having to construct a map out of `S¹`

that *is* dependent on `x`

:

```
example : (x : S¹) → doubleCover x → doubleCover x
example = {!!}
```

We intend for this map to flip each fiber `doubleCover x`

just like `Flip : Bool → Bool`

flips `Bool`

.

We could case on

`x`

like we did in the definition of`doubleCover`

, resulting inexample : (x : S¹) → doubleCover x → doubleCover x example base = {!!} example (loop i) = {!!}

Check and fill the first goal for the

`base`

case.## Solution

It asks for a map

`Bool → Bool`

since the fiber`doubleCover base`

is by definition`Bool`

. We give`Flip`

since we want it to flip each fiber.In the second case we need to give a map

`doubleCover (loop i) → doubleCover (loop i)`

, which by definition reduces to`flipPath i → flipPath i`

. It is not immediately obvious what we can do here. Case on things in`flipPath i`

is not an option for instance.

We should take a step back and notice what we have.
Firstly `λ i → doubleCover (loop i) → doubleCover (loop i)`

defines a path in the space of spaces
(it is a function space at each `i`

).
It starts and ends at `Bool → Bool`

.

On the other hand, the goal requires is a “path” starting
and ending at `Flip : Bool → Bool`

,
and being a point in `p i : doubleCover (loop i) → doubleCover (loop i)`

at each point.
It moves along *inside* the path of spaces
`λ i → doubleCover (loop i) → doubleCover (loop i)`

.
However, this “path” `p`

moving along inside the path of spaces
is *not* a path in a single space,
so we need to formalise this new notion.

Idea

What we need is a generalisation of paths : we need paths that can move between spaces, which we call “dependent paths”.

## Part 1 - Dependent Paths

### In general

Recall that if we have two spaces `A0 A1 : Type`

(e.g. both `Bool → Bool`

)
and a path `A : A0 ≡ A1`

between them
(e.g. `λ i → doubleCover (loop i) → doubleCover (loop i)`

),
then any point in `A0`

can be transported along the path `A`

to a point in `A1`

using `pathToFun`

a.k.a. `transport`

.
Since `A0`

and `A1`

are internally *equal*,
one might wonder if we can even consider what it means for points `x : A0`

and `y : A1`

to be *equal*, perhaps keeping the path `A`

in mind somehow
(e.g. `x`

and `y`

are both `Flip`

).
We are asking whether the notion of a *dependent path* -
in this case a path dependent on `A`

- can be made precise.
*Externally* `x`

and `y`

belong to different spaces
so it doesn’t make sense to ask for the path type `x ≡ y`

,
but HoTT and `cubical agda`

offer solutions to this.

In HoTT, a workaround is “say `x`

and `y`

are equal along `A`

when we have a path from `pathToFun A x`

to `y`

in the space `A1`

”
(note that we made a choice of a path in `A1`

here;
we could have done the same with `A0`

, with an inverted `pathToFun`

).
This is sensible, since `pathToFun A x`

is meant to be the point in `A1`

corresponding to `x`

under the identification of the spaces `A0`

and `A1`

given by `A`

.
Try to define this in `1FundamentalGroup/Quest5.agda`

.

## Solution

```
PathD : {A0 A1 : Type} (A : A0 ≡ A1) (x : A0) (y : A1) → Type
PathD A x y = pathToFun A x ≡ y
```

If you like, we can introduce suggestive notation for dependent paths,
but may be harder to read than `PathD`

:

```
syntax PathD A x y = x ≡ y along A
```

So now we can write `x ≡ y along A`

to mean paths from `x`

to `y`

dependent on the path `A`

.

There is a slightly different `cubical agda`

way of going about this.
Intuitively a path in `cubical agda`

is a starting point,
an ending point, and something in between that agrees on the boundary.
Thus a path dependent on `A : A0 ≡ A1`

from `x`

to `y`

can be
introduced by giving at each arbitrary `i : I`

on the “interval”
a point `t : A i`

such that `t`

is *externally equal to* `x`

at the start
and `y`

at the end.

```
PathP : (A : I → Type) → A i0 → A i1 → Type
```

`A`

takes each `i : I`

to a space `A i : Type`

,
so we can think of `A`

as a path.
Then `PathP`

takes `A`

, a point `x : A i0`

in the starting space and a point `y : A i1`

in the ending space, and gives the space of dependent paths
along `A`

.

We will try to mostly use the HoTT version of paths,
since HoTT is the main discussion here.
So we will assume that the two notions are the same
using an isomorphism `PathPIsoPathD`

from the library.

```
PathPIsoPath : (A : I → Type) (x : A i0) (y : A i1) →
(PathP A x y) ≅ (transport (λ i → A i) x ≡ y)
```

Let us continue with the example to understand how this works.

### Using Dependent Paths

Going back to our example,
we need to give a dependent path from `Flip`

to `Flip`

- dependent on the path `λ i → flipPath i → flipPath i`

in the space of spaces.
Let us extract this as a lemma :

```
example : (x : S¹) → doubleCover x → doubleCover x
example base = Flip
example (loop i) = p i where
p : PathP (λ i → flipPath i → flipPath i) Flip Flip
p = {!!}
```

At point `loop i`

on the loop, we give
the point `p i`

in `flipPath i → flipPath i`

.
Note that `PathP`

needs to know which path we are depending on,
and that is the first piece of data it takes in.

Now, instead of giving a `PathP`

, as `agda`

natively prefers,
we will give a `PathD`

, using `PathPIsoPathD`

.
`PathPIsoPathD`

will give us an isomorphism,
but we only want the map backwards -
taking a `PathD`

and giving us a `PathP`

.
To do so we write `_≅_.inv`

in the hole and refine.
It knows that the goal is a `PathP`

,
so it should reduce to

```
p : PathP (λ i → flipPath i → flipPath i) Flip Flip
p = _≅_.inv {!!} {!!}
```

Check the goals,
in the first it should now be asking for an isomorphism,
which we give by refining with `PathPIsoPathD`

,
the second hole depends on the first,
so it will make more sense when we can come back to it later.

```
p : PathP (λ i → flipPath i → flipPath i) Flip Flip
p = _≅_.inv (PathPIsoPathD {!!} {!!} {!!}) {!!}
```

Now try to give `PathPIsoPathD`

the necessary inputs.

## Solution

It just needs to know what path we want to be dependent over, the starting point, and the ending point.

```
p : PathP (λ i → flipPath i → flipPath i) Flip Flip
p = _≅_.inv (PathPIsoPathD (λ i → flipPath i → flipPath i) Flip Flip) {!!}
```

Checking the final hole we see that we need a path from the function
`pathToFun (λ i₁ → flipPath i₁ → flipPath i₁) Flip`

to the function `Flip`

.
This is now just a normal path in `Bool → Bool`

.
We refrain from spoiling the rest of the proof.

## Hint

To prove that two functions are the same we can use `funExt`

to just check they are the same at each point.
Naturally, we extract this as a lemma so that we can case on the point in `Bool`

.

Reminding ourselves of what `flipPath`

looks like, and what `pathToFun`

does,
we should be able to guess what the values on each side turn out to be.

## Solutions

```
example : (x : S¹) → doubleCover x → doubleCover x
example base = Flip
example (loop i) = p i where
lem : (x : Bool) → pathToFun (λ i → flipPath i → flipPath i) Flip x ≡ Flip x
lem false = refl
lem true = refl
p : PathP (λ i → flipPath i → flipPath i) Flip Flip
p = _≅_.inv (PathPIsoPathD (λ i → flipPath i → flipPath i) Flip Flip) (funExt lem)
```

### Mapping out of the circle

We might want to generalize the above process once and for all so that
we can map out the circle with greater ease.
We suggest that to map out of the circle into a bundle over the circle
``B : S¹ → Type`

,
it suffices to give a point `b : B base`

to map `base`

to,
and to give a `PathD`

dependent on `B`

and `loop`

which
starts and ends at `b`

.

Try to formalise and prove this in the quest.

## Hint

You need not, but we found it is convenient to define one for each
`PathP`

and `PathD`

.
The first is of course trivial.

```
outOfS¹P : (B : S¹ → Type) → (b : B base) → PathP (λ i → B (loop i)) b b → (x : S¹) → B x
outOfS¹P B b p base = b
outOfS¹P B b p (loop i) = p i
outOfS¹D : (B : S¹ → Type) → (b : B base) → b ≡ b along (λ i → B (loop i))
→ (x : S¹) → B x
outOfS¹D B b p x = {!!}
```

The next we can define using the first, using `PathPIsoPathD`

.

## Solution

```
outOfS¹D : (B : S¹ → Type) → (b : B base) → b ≡ b along (λ i → B (loop i))
→ (x : S¹) → B x
outOfS¹D B b p x = outOfS¹P B b (_≅_.inv (PathPIsoPathD (λ i → B (loop i)) b b) p) x
```

Cases / Induction / Recursors / Universal properties

In general, given a higher inductive type we will always have the above process, which can be interpreted in the following ways :

It is casing on where the term came from or where the proof came from. For example to map out of the proposition “

`A`

or`B`

” we can case on if the proof came from`A`

or from`B`

. To map out of “`A`

and`B`

” we can case on the proof and it must give us a pair, proving both.It is induction on the inductively defined type. This was exemplified in our discussion on the naturals.

It is the mapping out property of the type, commonly called

*the recursor*, and it just considers what recipes went into making the type. For example the only recipes that went into making the circle are`base`

and`loop`

.Often this can be seen as a universal property. For example the universal property of disjoint sums (a.k.a coproducts a.k.a “or”) can be seen as saying “to map out of

`A ⊔ B`

it suffices to give a map out of`A`

and a map out of`B`

”

We should verify that the this mapping out property does actually give us
what we expect.
For example, we gave it a point `b : B base`

to map `base`

.
We therefore should expect that it does map `base`

to `b`

.
Tracing through the definitions we have made,
we should be able to see this is true *externally*.

More explicitly

```
outOfS¹DBase : (B : S¹ → Type) (b : B base)
(p : b ≡ b along (λ i → B (loop i)))→ outOfS¹D B b p base ≡ b
outOfS¹DBase B b p = refl
```

## Part 2 - How `pathToFun`

Interacts with Other Types

When we are coming up with dependent paths between points in
equal spaces connected by some path `A`

,
we end up with needing some idea of what
`pathToFun`

looks like when it goes along the path.
For example, if `A`

were `λ i → B i → C i`

,
where `B`

and `C`

are respectfully paths between spaces,
then we might guess that we can describe `pathToFun B f`

more explicitly by checking what it does on points.

In this part we will consider different type constructions
and how paths between them convert to functions between them
via `pathToFun`

.
A detailed motivating example can be found
here.

### Function spaces

Suppose we have spaces `A0 A1 B0 B1 : Type`

and paths `A : A0 ≡ A1`

and `B : B0 ≡ B1`

.
Then let `pAB`

denote the path
`λ i → A i → B i : (A0 → B0) ≡ (A1 → B1)`

.
We want to figure out what `pathToFun`

does when it follows a function `f : A0 → B0`

along the path `pAB`

.

We know by functional extensionality that the function
`pathToFun pAB f : A1 → B1`

should be determined by what it does to terms in `A1`

,
so we can assume `a1 : A1`

.
The idea is we “apply `f`

by sending `a1`

back to `A0`

”.
Since `pathToFun (sym A) a1`

is meant to give the point in `A0`

that “looks like `a1`

”, we try applying `f`

to this point,
then send it across again via the path `B`

to the point
`f (pathToFun (sym A) a1)`

looks like in `B1`

.
We expect the outcome to be the same.

Try to formalize and prove this in `0Trinitarianism/Quest5.agda`

.

## The Statement

```
pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
pathToFun→ = {!!}
```

There are several ways to state the same idea. We didn’t have to reverse the path `A`

for example.

## Hint 0

We can induct on both `A`

and `B`

.

## Solution for Hint 0

```
J (λ A1 A → pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1)))
(
J (λ B1 B → pathToFun (λ i → A0 → B i) f ≡ λ a → pathToFun B (f (pathToFun (sym refl) a)))
(
pathToFun refl f
≡⟨ {!!} ⟩
(λ a → pathToFun refl (f (pathToFun (sym refl) a))) ∎
)
B
)
A
```

## Hint 1

There are many small equalities that are needed,
for example, we need how `sym`

and `refl`

interact
and what `pathToFun`

does to `refl`

.
At some point it would be useful to just check that
the functions are equal on terms.

## Solutions

```
pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
pathToFun→ {A0} {A1} {B0} {B1} {A} {B} f =
J (λ A1 A → pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1)))
(
J (λ B1 B → pathToFun (λ i → A0 → B i) f ≡ λ a → pathToFun B (f (pathToFun (sym refl) a)))
(
pathToFun refl f
≡⟨ pathToFunReflx f ⟩
f
≡⟨ funExt (λ a →
f a
≡⟨ cong f (sym (pathToFunReflx a)) ⟩
f (pathToFun refl a)
≡⟨ cong (λ p → f (pathToFun p a)) (sym symRefl) ⟩
f (pathToFun (sym refl) a)
≡⟨ sym (pathToFunReflx (f (pathToFun (sym refl) a))) ⟩
pathToFun refl (f (pathToFun (sym refl) a)) ∎
)
⟩
(λ a → pathToFun refl (f (pathToFun (sym refl) a))) ∎
)
B
)
A
```

### More to come in the future

This quest is a work in progress.