diff --git a/doc/cubical.tex b/doc/cubical.tex index d45c1fd..43446cd 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -149,7 +149,7 @@ this thesis. \TODO{Refer the reader somewhere for more info.} \section{Homotopy levels} In ITT all equality proofs are identical (in a closed context). This means that, in some sense, any two inhabitants of $a \equiv b$ are ``equally good'' -- they -don't have any interesting structure. This is referred to as Uniqueness of +do not have any interesting structure. This is referred to as Uniqueness of Identity Proofs (UIP). Unfortunately it is not possible to have a type-theory with both univalence and UIP. In stead we have a hierarchy of types with an increasing amount of homotopic structure. At the bottom of this hierarchy we @@ -192,9 +192,9 @@ indeed both $\top$ and $\bot$ are propositions: λ\varnothing\ \varnothing & \tp \isProp\ ⊥ \end{align*} % -I've used $\varnothing$ here to denote an impossible pattern. It is a theorem -that if a mere proposition $A$ is inhabited, then so is it contractible. If it -is not inhabited it is equivalent to the empty-type (or false +$\varnothing$ is used here to denote an impossible pattern. It is a theorem that +if a mere proposition $A$ is inhabited, then so is it contractible. If it is not +inhabited it is equivalent to the empty-type (or false proposition).\TODO{Cite!!} I will refer to a type $A \tp \MCU$ as a \emph{mere} proposition if I want to @@ -209,15 +209,15 @@ Then comes the set of homotopical sets: \end{aligned} \end{equation} % -I won't give an example of a set at this point. It turns out that proving e.g. -$\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). +I will not give an example of a set at this point. It turns out that proving +e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). There will be examples of sets later in this report. At this point it should be noted that the term ``set'' is somewhat conflated; there is the notion of sets from set-theory, in Agda types are denoted \texttt{Set}. I will use it -consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is -a proposition. +consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is a +proposition. -The next step in the hierarchy is, as the reader might've guessed, the type: +As the reader may have guessed the next step in the hierarchy is the type: % \begin{equation} \begin{aligned} @@ -278,8 +278,8 @@ We have the function: \pathJ\ P\ p \tp \prod_{a' \tp A} \prod_{p \tp a ≡ a'} P\ a\ p \end{equation} % -I will not give an example of using $\pathJ$ here. But we'll see an application -of it in \ref{eq:pathJ-example}. +I will not give an example of using $\pathJ$ here. An application can be found +later in \ref{eq:pathJ-example}. \subsection{Paths over propositions} \label{sec:lemPropF} diff --git a/doc/discussion.tex b/doc/discussion.tex index c7c6693..771d4ef 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -7,9 +7,9 @@ to very complicated goals. One technique for alleviating this was to prove that certain types are mere propositions. \subsection{Computational properties} -Another aspect (\TODO{That I actually didn't highlight very well in the previous - chapter}) is the computational nature of paths. Say we have formalized this -common result about monads: +Another aspect (\TODO{That I actually did not highlight very well in the + previous chapter}) is the computational nature of paths. Say we have +formalized this common result about monads: \TODO{Some equation\ldots} diff --git a/doc/implementation.tex b/doc/implementation.tex index 6e91000..93c404e 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -186,11 +186,11 @@ us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp set. This example illustrates nicely how we can use these combinators to reason about -`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined -at the other homotopic levels. These combinators are however not applicable in -situations where we want to reason about other types - e.g. types we've defined -ourselves. For instance, after we've proven that all the projections of -pre-categories are propositions, then we would like to bundle this up to show +`canonical' types like $\sum$ and $\prod$. Similar combinators can be defined at +the other homotopic levels. These combinators are however not applicable in +situations where we want to reason about other types - e.g. types we have +defined ourselves. For instance, after we have proven that all the projections +of pre-categories are propositions, then we would like to bundle this up to show that the type of pre-categories is also a proposition. Formally: % \begin{equation} @@ -208,8 +208,7 @@ Where The definition of $\IsPreCategory$ is the triple: % Each corresponding to the first three laws for categories. Note that since $\IsPreCategory$ is not formulated with a chain of sigma-types we wont have any -combinators available to help us here. In stead we'll have to use the path-type -directly. +combinators available to help us here. In stead the paths must be used directly. \ref{eq:propIsPreCategory} is judgmentally the same as % @@ -252,7 +251,7 @@ $i$ becomes the triple: \end{aligned} \end{equation} % -I've found this to be a general pattern when proving things in homotopy type +I have found this to be a general pattern when proving things in homotopy type theory, namely that you have to wrap and unwrap equalities at different levels. It is worth noting that proving this theorem with the regular inductive equality type would already not be possible, since we at least need extensionality (the @@ -287,7 +286,7 @@ latter. This is because $\isProp$ talks about non-dependent paths. So we need to 'promote' the result that univalence is a proposition to a heterogeneous path. To this end we can use $\lemPropF$, which was introduced in \S\ref{sec:lemPropF}. -In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We've +In this case $A = \var{IsIdentity}\ \identity$ and $B = \Univalent$. We have shown that being a category is a proposition, a result that holds for any choice of identity proof. Finally we must provide a proof that the identity proofs at $a$ and $b$ are indeed the same, this we can extract from $p$ by applying @@ -473,7 +472,7 @@ I will give the proof of the first theorem here, the second one is analogous. In the second step we use the fact that $p$ is constructed from the isomorphism $\iota$ -- $\inv{(\idToIso\ p)}$ denotes the map $B \to A$ induced by the isomorphism $\idToIso\ p \tp A \cong B$. The helper-lemma is similar to -what we're trying to prove but talks about paths rather than isomorphisms: +what we are trying to prove but talks about paths rather than isomorphisms: % \begin{equation} \label{eq:coeDomIso} @@ -524,9 +523,9 @@ And this finishes the proof of \ref{eq:coeDomIso} and thus \ref{eq:coeDom}. \section{Categories} \subsection{Opposite category} \label{op-cat} -The first category I'll present is a pure construction on categories. Given some -category we can construct its dual, called the opposite category. Starting with -a simple example allows us to focus on how we work with equivalences and +The first category I will present is a pure construction on categories. Given +some category we can construct its dual, called the opposite category. Starting +with a simple example allows us to focus on how we work with equivalences and univalence in a very simple category where the structure of the category is rather simple. @@ -537,7 +536,7 @@ an arrow from $B$ to $A$ in the underlying category. The identity arrow is the same as the one in the underlying category (they have the same type). Function composition will be reverse function composition from the underlying category. -I'll refer to things in terms of the underlying category, unless they have an +I will refer to things in terms of the underlying category, unless they have an over-bar. So e.g. $\idToIso$ is a function in the underlying category and the corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite category. @@ -613,9 +612,9 @@ $$ \prod_{\bC \tp \Category} \left(\bC^{\var{Op}}\right)^{\var{Op}} \equiv \bC $$ % -As we've seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite -involved.\footnote{We haven't even seen the full story because we've used this - `interface' for equivalences.} Luckily since being-a-category is a mere +As we have seen the laws in $\left(\bC^{\var{Op}}\right)^{\var{Op}}$ get quite +involved.\footnote{We have not even seen the full story because we have used + this `interface' for equivalences.} Luckily since being-a-category is a mere proposition, we need not concern ourselves with this bit when proving the above. We can use the equality principle for categories that let us prove an equality just by giving an equality on the data-part. So, given a category $\bC$ all we @@ -794,8 +793,9 @@ is later extended to talk about higher categories. \section{Products} \label{sec:products} -In the following I'll demonstrate a technique for using categories to prove -properties. The goal in this section is to show that products are propositions: +In the following a technique for using categories to prove properties will be +demonstrated. The goal in this section is to show that products are +propositions: % $$ \prod_{\bC \tp \Category} \prod_{A\;B \tp \Object} \isProp\ (\var{Product}\ \bC\ A\ B) @@ -806,7 +806,7 @@ and $B$ in the category $\bC$. I do this by constructing a category whose terminal objects are equivalent to products in $\bC$, and since terminal objects are propositional in a proper category and equivalences preserve homotopy level, then we know that products also are propositions. But before we get to that, -let's recall the definition of products. +we recall the definition of products. \subsection{Definition of products} Given a category $\bC$ and two objects $A$ and $B$ in $\bC$ we define the @@ -1080,8 +1080,8 @@ equality principle for arrows in this category (\ref{eq:productEqPrinc}) gives us that it suffices to show that $f$ and $\inv{f}$, this is exactly $\var{inv}_f$. -This concludes the first direction of the isomorphism that we're constructing. -For the other direction we're given just given the isomorphism +This concludes the first direction of the isomorphism that we are constructing. +For the other direction we are given the isomorphism: % $$ (f, \inv{f}, \var{inv}_f) @@ -1151,7 +1151,7 @@ gory details. % \subsection{Propositionality of products} % -Now that we've constructed the ``pair category'' I'll demonstrate how to use +Now that we have constructed the ``pair category'' I will demonstrate how to use this to prove that products are propositional. I will do this by showing that terminal objects in this category are equivalent to products: % @@ -1162,7 +1162,7 @@ terminal objects in this category are equivalent to products: And as always we do this by constructing an isomorphism: % In the direction $\var{Terminal} → \var{Product}\ ℂ\ \mathcal{A}\ \mathcal{B}$ -we're given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and +we are given a terminal object $X, x_𝒜, x_ℬ$. $X$ Will be the product-object and $x_𝒜, x_ℬ$ will be the product arrows, so it just remains to verify that this is indeed a product. That is, for an object $Y$ and two arrows $y_𝒜 \tp \Arrow\ Y\ 𝒜$, $y_ℬ\ \Arrow\ Y\ ℬ$ we must find a unique arrow $f \tp diff --git a/doc/introduction.tex b/doc/introduction.tex index 6dc252b..cc86d90 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -30,7 +30,7 @@ Consider the functions: \end{multicols} % $n + 0$ is \nomen{definitionally} equal to $n$, which we write as $n + 0 = n$. -This is also called \nomen{judgmental} equality. We call it definitional +This is also \called \nomen{judgmental} equality. We call it definitional equality because the \emph{equality} arises from the \emph{definition} of $+$ which is: % @@ -56,7 +56,7 @@ equivalence of $f$ and $g$ -- even though we can prove them equal for all points. This is exactly the notion of equality of functions that we are interested in; that they are equal for all inputs. We call this \nomen{point-wise equality}, where the \emph{points} of a function refers -to it's arguments. +to its arguments. In the context of category theory functional extensionality is e.g. needed to show that representable functors are indeed functors. The representable functor diff --git a/doc/sources.tex b/doc/sources.tex index 080e875..772a037 100644 --- a/doc/sources.tex +++ b/doc/sources.tex @@ -3,7 +3,7 @@ In the following a few of the definitions mentioned in the report are included. The following is \emph{not} a verbatim copy of individual modules from the implementation. Rather, this is a redacted and pre-formatted designed for -presentation purposes. It's provided here as a convenience. The actual sources +presentation purposes. Its provided here as a convenience. The actual sources are the only authoritative source. Is something is not clear, please refer to those. \section{Cubical}