I've decided this morning to learn a bit of Agda.
Here's what I've done today, it goes through chapter 2 proving everything in Agda by staying as close as possible to the book (for example when multiple proof terms worked, I choose the one from the book).
I also choose to stay away from implicit propositional equality, with its powerful refl induction. The reason for this is that it looks like Agda is doing all the work and in the end, I still don't understand why things work.
Here is the agda file. It is self-contained but I've stopped at 2.4.7.
IdentityTypes.agda
Sunday, November 17, 2013
Saturday, November 16, 2013
2.3 -- An explanation of "Type families as fibrations" using diagrams (Part 1)
I'm often in need of diagrams for understanding abstract concepts. I perfectly understand why there's not a lot of diagram in HOTT book : it was made in a very short time to explain the theory in the doing.
Here I'll try to re-explain 2.3 using diagrams. I will stay very close to the book material.
Here we can display the type family $P$ using this diagram :
where to each element we have associated a whole type.
Elements of type $\sum_{a:A} P(a)$ can be displayed as pairings preserving those yellow arrows :
Take an onto morphism between vector spaces $f : X \rightarrow Y$, we can define the mapping $g$ over $Y$ by setting $g(y) = f^{(-1)}(x) = \{ x \in X ~|~ f(x) = y \}$. Each $g(y)$ is called the fiber over $y$. All fibers are affine subspace of $Y$ with the same direction $Ker(f)$.
The space $Y$ is called the base space of $f$ because the defining element of each fiber lives there. The space $X$ is called the total space because its the disjoint union of all the fibers.
Now, let's take a path from $y$ to $y'$ in $Y$. I.e. a continuous mapping $p : [0,1] \rightarrow Y$ such that $p(0) = y$ and $p(1) = y'$. Note that this is a trivial case of homotopy between two constants functions.
Taking a starting point $u$ in the fiber over $y$. We can try to lift this path in a path $p_*$ in the total space $X$ by walking through fibers starting in $u$ and by mimicking the path $p$. If such a map is guaranteed to exists we say that $f$ is a fibration.
Here we can explicitly define this map. Take $E$ to be such that $Ker f \oplus E = X$ and $u \in E$. The map $f_{|E}$ is an isomorphism from $E$ to $Y$. We can set $p_* = f_{|E}^{-1} p$. We have $p_*(0) = f_{|E}^{-1}(y) = u$ and $p_*$ is continuous because it's the compound of a linear, hence continuous, map and the continuous map $p$. Note that $p_*(1) = f_{|E|}^{-1}(y')$ and $f(p_*(1)) = y'$ so $p_*(1)$ in the fiber over $y'$.
This situation is depicted here :
(What we have described here is the structure of a trivial vector bundle.)
One of the most important fact of homotopy theory is that given two elements $x, y : A$, a proof $p : x = y$ of equality between those two elements can be interpreted as a path from $x$ to $y$.
The fibration property would ensure that given $u : P(x)$ we could define a path $p'$ starting at $(x,u)$ in the total space $\sum_{a:A} P(a)$. There's no way of knowing in which fibers would this path walk, but what is certain is that its ending point has to be of the form $(y, v)$ with $v : P(y)$.
If we sum it up, what we want to construct is a function $transport_p : P(x) \rightarrow P(y)$. We can construct it by path induction by assuming that $p \equiv refl_x$ and thus $x \equiv y$. The function we want in this case has to go from $P(x)$ to itself, therefore we can set it to be $id_{P(x)}$ and we are done.
We note $p_*(u) = transport_p(u)$. And it is depicted here : .
To get back the full fibration property we need to show that $p$ itself can be lifted to a path $lift(p,u) : (x,u) =_{\sum_{a:A} P(a)} (y,p_*(u))$. By path induction, we can assume that $p \equiv refl_x$ and that $x \equiv y$. Then we need to build a path $(x,u) = (x,u)$ as $p_* = id$ in this case. We can take $refl_{(x,u)}$ and it concludes the proof.
Here this path is depicted between the boxed elements of $\sum_{x:A} P(x)$ :
Here I'll try to re-explain 2.3 using diagrams. I will stay very close to the book material.
2.3 -- An explanation of "Type families as fibrations" using diagrams (Part 1)
Type families
A type family is the basis of the definition of a dependent pair. It's a function $P : A \rightarrow \mathcal{U}$ for a type $A$ and an universe $\mathcal{U}$. Using this function we can define the type of dependent pair $\sum_{x:A} P(x)$ with the basic construction $(a,b)$ taking an element $a: A$ and an element $b: P(a)$. As $b$ in the pair depends on the first component, it's called a dependent pair.Here we can display the type family $P$ using this diagram :
Elements of type $\sum_{a:A} P(a)$ can be displayed as pairings preserving those yellow arrows :
Fibrations
Before explaining why such a type family is a fibration, I'll recall what is a fibration through the most trivial example.Take an onto morphism between vector spaces $f : X \rightarrow Y$, we can define the mapping $g$ over $Y$ by setting $g(y) = f^{(-1)}(x) = \{ x \in X ~|~ f(x) = y \}$. Each $g(y)$ is called the fiber over $y$. All fibers are affine subspace of $Y$ with the same direction $Ker(f)$.
The space $Y$ is called the base space of $f$ because the defining element of each fiber lives there. The space $X$ is called the total space because its the disjoint union of all the fibers.
Now, let's take a path from $y$ to $y'$ in $Y$. I.e. a continuous mapping $p : [0,1] \rightarrow Y$ such that $p(0) = y$ and $p(1) = y'$. Note that this is a trivial case of homotopy between two constants functions.
Taking a starting point $u$ in the fiber over $y$. We can try to lift this path in a path $p_*$ in the total space $X$ by walking through fibers starting in $u$ and by mimicking the path $p$. If such a map is guaranteed to exists we say that $f$ is a fibration.
Here we can explicitly define this map. Take $E$ to be such that $Ker f \oplus E = X$ and $u \in E$. The map $f_{|E}$ is an isomorphism from $E$ to $Y$. We can set $p_* = f_{|E}^{-1} p$. We have $p_*(0) = f_{|E}^{-1}(y) = u$ and $p_*$ is continuous because it's the compound of a linear, hence continuous, map and the continuous map $p$. Note that $p_*(1) = f_{|E|}^{-1}(y')$ and $f(p_*(1)) = y'$ so $p_*(1)$ in the fiber over $y'$.
This situation is depicted here :
(What we have described here is the structure of a trivial vector bundle.)
Type family as fibration
Looking back at the type family $P : A \rightarrow \mathcal{U}$ we can see that $P(x)$ looks just like a fiber with base point $x$. So we could think of $A$ as a base space. The total space is the union of all fibers, therefore it would be here $\sum_{x:A} P(x)$. We don't really have a candidate for a fibration but it doesn't prevent us from looking at the fibration defining property in this setting.One of the most important fact of homotopy theory is that given two elements $x, y : A$, a proof $p : x = y$ of equality between those two elements can be interpreted as a path from $x$ to $y$.
The fibration property would ensure that given $u : P(x)$ we could define a path $p'$ starting at $(x,u)$ in the total space $\sum_{a:A} P(a)$. There's no way of knowing in which fibers would this path walk, but what is certain is that its ending point has to be of the form $(y, v)$ with $v : P(y)$.
If we sum it up, what we want to construct is a function $transport_p : P(x) \rightarrow P(y)$. We can construct it by path induction by assuming that $p \equiv refl_x$ and thus $x \equiv y$. The function we want in this case has to go from $P(x)$ to itself, therefore we can set it to be $id_{P(x)}$ and we are done.
We note $p_*(u) = transport_p(u)$. And it is depicted here : .
Here this path is depicted between the boxed elements of $\sum_{x:A} P(x)$ :
2.7 -- Functoriality of ap under $\sum$-types
(I won't start with the introduction of HOTT, as it very well explained here http://homotopytypetheory.org/book/ . Instead, I'll present what was lately on my scratchpad.)
First, let's recall what happens for a cartesian product. To build a function $f : A \times B \rightarrow A' \times B'$ we can join two functions $g : A \rightarrow A'$ and $h : B \rightarrow B'$ in the following way : for every $x \in A \times B$ we set $f(x) :\equiv (g(pr_1(x)), h(pr_2(y)))$. What is done is a split of $x$ into its components on which we apply separately $g$ and $h$.
To extend this definition to $\sum$-type, given two type families $P : A \rightarrow \mathcal{U}$ and $P' : A' \rightarrow \mathcal{U}'$, we want to build a function $f : \sum_{x : A} P(x) \rightarrow \sum_{x' : A'} P'(x')$ by joining two functions applied component-wise. The first function is straightforward to type : we reuse $g : A \rightarrow A'$. But, for the second function we can't take one unrelated to $g$. The reason for this lies in the result of $f$, as it will make a dependent pair of the form $( g(pr_1(x)), h(pr_2(x)))$ for it to inhabit the type $\sum_{x':A'} P'(x')$ we must have the typing $h(pr_2(x)) : P'(g(pr_1(x)))$, Therefore, the type of $h$ must depend on $g(pr_1(x))$! Then to get this dependency, the simplest approach is to have $h(a,a') : P(a) \rightarrow P'(a')$ but we could have taken $h(a,g) : P(a) \rightarrow P'(g(a))$. I think the first type is more general, but the second one makes a stronger theorem because it's easier to build this kind of $h$ as it doesn't need to provide functions when $a' \neq g(a)$.
Our definition of $f$ is then like this : take $g : A \rightarrow A'$ and $h : \prod_{a : A} P(a) \rightarrow P'(g(a))$, we can then define
\[
f(x) :\equiv (g(pr_1(x)), h(pr_1(x), pr_2(x)))
\]
(Note here that I'm unsure of the type of $h$, one could argue that $h : \prod_{g : A' \rightarrow A} \prod_{a : A} P(a) \rightarrow P'(g(a))$ would be clearer as it removes the explicit dependency of $h$ over $g$. But, for me, it means that such $h$ is infinitely harder to build because it needs to be defined for every possible $g$!)
It remains to state the equivalent of theorem 2.6.5 in this context. Recall that the equality $q : pr_2(x) = pr_2(y)$ needs to be transported in the right space as $pr_2(x) : P(pr_1(x))$ and $pr_2(y) : P(pr_1(y))$. We can set it to happen in $P(pr_1(y))$ but we have to transport $pr_2(x)$ there using $transport^P(p,pr_2(x)) = p_*(pr_2(x))$ where $p : pr_1(x) = pr_1(y)$.
Theorem 2.7.5 : In the above situation, given $x, y : \sum_{a:A} P(a)$ and $p : pr_1(x) = pr_1(y)$ and $q : p_*(pr_2(x)) = pr_2(y)$, we have
\[
f(pair^=(p,q)) =_{(f(x)=f(y))} pair^=(g(p), h(pr_1(y), q))
\]
Proof.By induction we can assume that $x \equiv (a,b)$ and $y \equiv (a',b')$. Then $p : a = a'$ and we can assume that $p \equiv refl_a$ by path induction. We now have $p_* \equiv id_{P(a)}$ and $q : b = b'$. We can assume that $q \equiv refl_b$ by path induction. At this point the left member of the equality is
\[
f(pair^=(refl_a, refl_b)) \equiv f(refl_{(a,b)} \equiv refl_{f(a,b)}
\]
and the right member is
\[
pair^=( g(refl_a), h(a, refl_b) ) \equiv pair^=(refl_{g(a)}, refl_{h(a, b)}) \equiv refl_{(g(a), h(a,b))} \equiv refl_{f(a,b)}
\]
So we now need a proof of the theorem in this case, but we already have one : $refl_{refl_{f(a,b)}}$.
2.7 -- Functoriality of ap under $\sum$-types
The statement of this theorem and its proof was left to the reader and it gave me some trouble to state it right.First, let's recall what happens for a cartesian product. To build a function $f : A \times B \rightarrow A' \times B'$ we can join two functions $g : A \rightarrow A'$ and $h : B \rightarrow B'$ in the following way : for every $x \in A \times B$ we set $f(x) :\equiv (g(pr_1(x)), h(pr_2(y)))$. What is done is a split of $x$ into its components on which we apply separately $g$ and $h$.
To extend this definition to $\sum$-type, given two type families $P : A \rightarrow \mathcal{U}$ and $P' : A' \rightarrow \mathcal{U}'$, we want to build a function $f : \sum_{x : A} P(x) \rightarrow \sum_{x' : A'} P'(x')$ by joining two functions applied component-wise. The first function is straightforward to type : we reuse $g : A \rightarrow A'$. But, for the second function we can't take one unrelated to $g$. The reason for this lies in the result of $f$, as it will make a dependent pair of the form $( g(pr_1(x)), h(pr_2(x)))$ for it to inhabit the type $\sum_{x':A'} P'(x')$ we must have the typing $h(pr_2(x)) : P'(g(pr_1(x)))$, Therefore, the type of $h$ must depend on $g(pr_1(x))$! Then to get this dependency, the simplest approach is to have $h(a,a') : P(a) \rightarrow P'(a')$ but we could have taken $h(a,g) : P(a) \rightarrow P'(g(a))$. I think the first type is more general, but the second one makes a stronger theorem because it's easier to build this kind of $h$ as it doesn't need to provide functions when $a' \neq g(a)$.
Our definition of $f$ is then like this : take $g : A \rightarrow A'$ and $h : \prod_{a : A} P(a) \rightarrow P'(g(a))$, we can then define
\[
f(x) :\equiv (g(pr_1(x)), h(pr_1(x), pr_2(x)))
\]
(Note here that I'm unsure of the type of $h$, one could argue that $h : \prod_{g : A' \rightarrow A} \prod_{a : A} P(a) \rightarrow P'(g(a))$ would be clearer as it removes the explicit dependency of $h$ over $g$. But, for me, it means that such $h$ is infinitely harder to build because it needs to be defined for every possible $g$!)
It remains to state the equivalent of theorem 2.6.5 in this context. Recall that the equality $q : pr_2(x) = pr_2(y)$ needs to be transported in the right space as $pr_2(x) : P(pr_1(x))$ and $pr_2(y) : P(pr_1(y))$. We can set it to happen in $P(pr_1(y))$ but we have to transport $pr_2(x)$ there using $transport^P(p,pr_2(x)) = p_*(pr_2(x))$ where $p : pr_1(x) = pr_1(y)$.
Theorem 2.7.5 : In the above situation, given $x, y : \sum_{a:A} P(a)$ and $p : pr_1(x) = pr_1(y)$ and $q : p_*(pr_2(x)) = pr_2(y)$, we have
\[
f(pair^=(p,q)) =_{(f(x)=f(y))} pair^=(g(p), h(pr_1(y), q))
\]
Proof.By induction we can assume that $x \equiv (a,b)$ and $y \equiv (a',b')$. Then $p : a = a'$ and we can assume that $p \equiv refl_a$ by path induction. We now have $p_* \equiv id_{P(a)}$ and $q : b = b'$. We can assume that $q \equiv refl_b$ by path induction. At this point the left member of the equality is
\[
f(pair^=(refl_a, refl_b)) \equiv f(refl_{(a,b)} \equiv refl_{f(a,b)}
\]
and the right member is
\[
pair^=( g(refl_a), h(a, refl_b) ) \equiv pair^=(refl_{g(a)}, refl_{h(a, b)}) \equiv refl_{(g(a), h(a,b))} \equiv refl_{f(a,b)}
\]
So we now need a proof of the theorem in this case, but we already have one : $refl_{refl_{f(a,b)}}$.
Subscribe to:
Posts (Atom)