From e5d55c7b2b115483c3a39222f3b58cb1a346245c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 16:22:51 +0200 Subject: [PATCH] Include appendices --- doc/cubical.tex | 3 + doc/implementation.tex | 5 + doc/introduction.tex | 2 +- doc/main.tex | 1 + doc/packages.tex | 31 ++- doc/sources.tex | 428 +++++++++++++++++++++++++++++++++++++++++ 6 files changed, 468 insertions(+), 2 deletions(-) create mode 100644 doc/sources.tex diff --git a/doc/cubical.tex b/doc/cubical.tex index d25054d..8ccd666 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -10,6 +10,9 @@ Cubical Agda extends the underlying type system (\TODO{Cite someone smarter than me with a good resource on this}) but introduces a data-type within the languages. +Exceprts of the source code relevant to this section can be found in appendix +\ref{sec:app-cubical}. + \subsection{The equality type} The usual notion of judgmental equality says that given a type $A \tp \MCU$ and two points of $A$; $a_0, a_1 \tp A$ we can form the type: diff --git a/doc/implementation.tex b/doc/implementation.tex index c5f01f7..2ce0d4e 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -50,6 +50,11 @@ where one can reason about two categories by simply focusing on the data. This is achieved by creating a function embodying the ``equality principle'' for a given type. +For the rest of this chapter I will present some of these results. For didactic +reasons no source-code has been included in this chapter. To see the formal +definitions excerpts of the implementation have been included in appendix +\ref{ch:app-sources}. + \section{Categories} The data for a category consist of a type for the sort of objects; a type for the sort of arrows; an identity arrow and a composition operation for arrows. diff --git a/doc/introduction.tex b/doc/introduction.tex index a8c19b5..12ad3b3 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -195,7 +195,7 @@ Name & Agda & Notation \\ \nomen{Type} & \texttt{Set} & $\Type$ \\ \nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\ Function, morphism, map & \texttt{A → B} & $A → B$ \\ -Dependent- ditto & \texttt{(a \tp A) → B} & $∏_{a \tp A} B$ \\ +Dependent- ditto & \texttt{(a : A) → B} & $∏_{a \tp A} B$ \\ \nomen{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\ \nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\ Definition & \texttt{=} & $̱\defeq$ \\ diff --git a/doc/main.tex b/doc/main.tex index a74978c..917f74d 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -69,6 +69,7 @@ \begin{appendices} \setcounter{page}{1} \pagenumbering{roman} +\input{sources.tex} %% \input{planning.tex} %% \input{halftime.tex} \end{appendices} diff --git a/doc/packages.tex b/doc/packages.tex index f592a65..19837af 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -15,7 +15,7 @@ \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage[toc,page]{appendix} \usepackage{xspace} -\usepackage{geometry} +\usepackage[a4paper]{geometry} % \setlength{\parskip}{10pt} @@ -37,6 +37,7 @@ \usepackage{lmodern} \usepackage{enumerate} +\usepackage{verbatim} \usepackage{fontspec} \usepackage[light]{sourcecodepro} @@ -56,3 +57,31 @@ %% \RequirePackage{kvoptions} \usepackage{pgffor} +\lstset + {basicstyle=\ttfamily + ,columns=fullflexible + ,breaklines=true + ,inputencoding=utf8 + ,extendedchars=true + %% ,literate={á}{{\'a}}1 {ã}{{\~a}}1 {é}{{\'e}}1 + } + +\usepackage{newunicodechar} + +%% \setmainfont{PT Serif} +\newfontfamily{\fallbackfont}{FreeMono.otf}[Scale=MatchLowercase] +%% \setmonofont[Mapping=tex-text]{FreeMono.otf} +\DeclareTextFontCommand{\textfallback}{\fallbackfont} +\newunicodechar{∨}{\textfallback{∨}} +\newunicodechar{∧}{\textfallback{∧}} +\newunicodechar{⊔}{\textfallback{⊔}} +\newunicodechar{≊}{\textfallback{≊}} +\newunicodechar{∈}{\textfallback{∈}} +\newunicodechar{ℂ}{\textfallback{ℂ}} +\newunicodechar{∘}{\textfallback{∘}} +\newunicodechar{⟨}{\textfallback{⟨}} +\newunicodechar{⟩}{\textfallback{⟩}} +\newunicodechar{∎}{\textfallback{∎}} +\newunicodechar{𝒜}{\textfallback{?}} +\newunicodechar{ℬ}{\textfallback{?}} +%% \newunicodechar{≊}{\textfallback{≊}} diff --git a/doc/sources.tex b/doc/sources.tex new file mode 100644 index 0000000..d270c1f --- /dev/null +++ b/doc/sources.tex @@ -0,0 +1,428 @@ +\chapter{Source code} +\label{ch:app-sources} +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 +are the only authoritative source. Is something is not clear, please refer to +those. +\clearpage +\section{Cubical} +\label{sec:app-cubical} +\begin{figure}[h] +\begin{Verbatim} +postulate + PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ + +module _ {ℓ} {A : Set ℓ} where + _≡_ : A → A → Set ℓ + _≡_ {A = A} = PathP (λ _ → A) + + refl : {x : A} → x ≡ x + refl {x = x} = λ _ → x +\end{Verbatim} +\caption{Excerpt from the cubical library. Definition of the path-type.} +\end{figure} +% +\begin{figure}[h] +\begin{Verbatim} +module _ {ℓ : Level} (A : Set ℓ) where + isContr : Set ℓ + isContr = Σ[ x ∈ A ] (∀ y → x ≡ y) + + isProp : Set ℓ + isProp = (x y : A) → x ≡ y + + isSet : Set ℓ + isSet = (x y : A) → (p q : x ≡ y) → p ≡ q + + isGrpd : Set ℓ + isGrpd = (x y : A) → (p q : x ≡ y) → (a b : p ≡ q) → a ≡ b +\end{Verbatim} +\caption{Excerpt from the cubical library. Definition of the first few + homotopy-levels.} +\end{figure} +% +\begin{figure}[h] +\begin{Verbatim} +module _ {ℓ ℓ'} {A : Set ℓ} {x : A} + (P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where + pathJ : (y : A) → (p : x ≡ y) → P y p + pathJ _ p = transp (λ i → uncurry P (contrSingl p i)) d +\end{Verbatim} +\clearpage +\caption{Excerpt from the cubical library. Definition of based path-induction.} +\end{figure} +% +\begin{figure}[h] +\begin{Verbatim} +module _ {ℓ ℓ'} {A : Set ℓ} {B : A → Set ℓ'} where + propPi : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x) + propPi h f0 f1 = λ i → λ x → (h x (f0 x) (f1 x)) i + + lemPropF : (P : (x : A) → isProp (B x)) {a0 a1 : A} + (p : a0 ≡ a1) {b0 : B a0} {b1 : B a1} → PathP (λ i → B (p i)) b0 b1 + lemPropF P p {b0} {b1} = λ i → P (p i) + (primComp (λ j → B (p (i ∧ j)) ) (~ i) (λ _ → λ { (i = i0) → b0 }) b0) + (primComp (λ j → B (p (i ∨ ~ j)) ) (i) (λ _ → λ{ (i = i1) → b1 }) b1) i + + lemSig : (pB : (x : A) → isProp (B x)) + (u v : Σ A B) (p : fst u ≡ fst v) → u ≡ v + lemSig pB u v p = λ i → (p i) , ((lemPropF pB p) {snd u} {snd v} i) + + propSig : (pA : isProp A) (pB : (x : A) → isProp (B x)) → isProp (Σ A B) + propSig pA pB t u = lemSig pB t u (pA (fst t) (fst u)) +\end{Verbatim} +\caption{Excerpt from the cubical library. A few combinators.} +\end{figure} +\clearpage +\section{Categories} +\label{sec:app-categories} +\begin{figure}[h] +\begin{Verbatim} +record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where + field + Object : Set ℓa + Arrow : Object → Object → Set ℓb + identity : {A : Object} → Arrow A A + _<<<_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C + + _>>>_ : {A B C : Object} → (Arrow A B) → (Arrow B C) → Arrow A C + f >>> g = g <<< f + + IsAssociative : Set (ℓa ⊔ ℓb) + IsAssociative = ∀ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D} + → h <<< (g <<< f) ≡ (h <<< g) <<< f + + IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb) + IsIdentity id = {A B : Object} {f : Arrow A B} + → id <<< f ≡ f × f <<< id ≡ f + + ArrowsAreSets : Set (ℓa ⊔ ℓb) + ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) + + IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb + IsInverseOf = λ f g → g <<< f ≡ identity × f <<< g ≡ identity + + Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb + Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g + + _≊_ : (A B : Object) → Set ℓb + _≊_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f) + + IsTerminal : Object → Set (ℓa ⊔ ℓb) + IsTerminal T = {X : Object} → isContr (Arrow X T) + + Terminal : Set (ℓa ⊔ ℓb) + Terminal = Σ Object IsTerminal +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category}. The definition of a category.} +\end{figure} +\clearpage +\begin{figure}[h] +\begin{Verbatim} +module Univalence (isIdentity : IsIdentity identity) where + idIso : (A : Object) → A ≊ A + idIso A = identity , identity , isIdentity + + idToIso : (A B : Object) → A ≡ B → A ≊ B + idToIso A B eq = subst eq (idIso A) + + Univalent : Set (ℓa ⊔ ℓb) + Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B) +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category}. Continued from previous. Definition of univalence.} +\end{figure} +\begin{figure}[h] +\begin{Verbatim} +module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where + record IsPreCategory : Set (lsuc (ℓa ⊔ ℓb)) where + open RawCategory ℂ public + field + isAssociative : IsAssociative + isIdentity : IsIdentity identity + arrowsAreSets : ArrowsAreSets + open Univalence isIdentity public + + record PreCategory : Set (lsuc (ℓa ⊔ ℓb)) where + field + isPreCategory : IsPreCategory + open IsPreCategory isPreCategory public + + record IsCategory : Set (lsuc (ℓa ⊔ ℓb)) where + field + isPreCategory : IsPreCategory + open IsPreCategory isPreCategory public + field + univalent : Univalent +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category}. Records with inhabitants for + the laws defined in the previous listings.} +\end{figure} +\clearpage +\begin{figure}[h] +\begin{Verbatim} +module Opposite {ℓa ℓb : Level} where + module _ (ℂ : Category ℓa ℓb) where + private + module _ where + module ℂ = Category ℂ + opRaw : RawCategory ℓa ℓb + RawCategory.Object opRaw = ℂ.Object + RawCategory.Arrow opRaw = flip ℂ.Arrow + RawCategory.identity opRaw = ℂ.identity + RawCategory._<<<_ opRaw = ℂ._>>>_ + + open RawCategory opRaw + + isPreCategory : IsPreCategory opRaw + IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative + IsPreCategory.isIdentity isPreCategory = swap ℂ.isIdentity + IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets + + open IsPreCategory isPreCategory + + ---------------------------- + -- NEXT LISTING GOES HERE -- + ---------------------------- + + isCategory : IsCategory opRaw + IsCategory.isPreCategory isCategory = isPreCategory + IsCategory.univalent isCategory + = univalenceFromIsomorphism (isoToId* , inv) + + opposite : Category ℓa ℓb + Category.raw opposite = opRaw + Category.isCategory opposite = isCategory + + module _ {ℂ : Category ℓa ℓb} where + open Category ℂ + private + rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw + RawCategory.Object (rawInv _) = Object + RawCategory.Arrow (rawInv _) = Arrow + RawCategory.identity (rawInv _) = identity + RawCategory._<<<_ (rawInv _) = _<<<_ + + oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ + oppositeIsInvolution = Category≡ rawInv +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category}. Showing that the opposite + category is a category. Part of this listing has been cut out and placed in + the next listing.} +\end{figure} +\clearpage +For reasons of formatting the following listing is continued from the above with +fewer levels of indentation. +% +\begin{figure}[h] +\begin{Verbatim} +module _ {A B : ℂ.Object} where + open Σ (toIso _ _ (ℂ.univalent {A} {B})) + renaming (fst to idToIso* ; snd to inv*) + open AreInverses {f = ℂ.idToIso A B} {idToIso*} inv* + + shuffle : A ≊ B → A ℂ.≊ B + shuffle (f , g , inv) = g , f , inv + + shuffle~ : A ℂ.≊ B → A ≊ B + shuffle~ (f , g , inv) = g , f , inv + + isoToId* : A ≊ B → A ≡ B + isoToId* = idToIso* ∘ shuffle + + inv : AreInverses (idToIso A B) isoToId* + inv = + ( funExt (λ x → begin + (isoToId* ∘ idToIso A B) x + ≡⟨⟩ + (idToIso* ∘ shuffle ∘ idToIso A B) x + ≡⟨ cong (λ φ → φ x) + (cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt (isoEq refl))) ⟩ + (idToIso* ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x + ≡⟨⟩ + (idToIso* ∘ ℂ.idToIso A B) x + ≡⟨ (λ i → verso-recto i x) ⟩ + x ∎) + , funExt (λ x → begin + (idToIso A B ∘ idToIso* ∘ shuffle) x + ≡⟨ cong (λ φ → φ x) + (cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt (isoEq refl))) ⟩ + (shuffle~ ∘ ℂ.idToIso A B ∘ idToIso* ∘ shuffle) x + ≡⟨ cong (λ φ → φ x) + (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩ + (shuffle~ ∘ shuffle) x + ≡⟨⟩ + x ∎) + ) +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category}. Proving univalence for the opposite category.} +\end{figure} +\clearpage +\section{Products} +\label{sec:app-products} +\begin{figure}[h] +\begin{Verbatim} +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + open Category ℂ + + module _ (A B : Object) where + record RawProduct : Set (ℓa ⊔ ℓb) where + no-eta-equality + field + object : Object + fst : ℂ [ object , A ] + snd : ℂ [ object , B ] + + record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where + open RawProduct raw public + field + ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) + → ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g) + + record Product : Set (ℓa ⊔ ℓb) where + field + raw : RawProduct + isProduct : IsProduct raw + + open IsProduct isProduct public + +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category.Product}. Definition of products.} +\end{figure} +% +\begin{figure}[h] +\begin{Verbatim} +module _{ℓa ℓb : Level} {ℂ : Category ℓa ℓb} + (let module ℂ = Category ℂ) {A* B* : ℂ.Object} where + + module _ where + raw : RawCategory _ _ + raw = record + { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X A* × ℂ.Arrow X B* + ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1) + → Σ[ f ∈ ℂ.Arrow A B ] + ℂ [ b0 ∘ f ] ≡ a0 + × ℂ [ b1 ∘ f ] ≡ a1 + } + ; identity = λ{ {X , f , g} + → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity + } + ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} + (f , f0 , f1) (g , g0 , g1) + → (f ℂ.<<< g) + , (begin + ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ + ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩ + ℂ [ b0 ∘ g ] ≡⟨ g0 ⟩ + a0 ∎ + ) + , (begin + ℂ [ c1 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ + ℂ [ ℂ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f1 ⟩ + ℂ [ b1 ∘ g ] ≡⟨ g1 ⟩ + a1 ∎ + ) + } + } +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category.Product}. Definition of ``pair category''.} +\end{figure} +\clearpage +\section{Monads} +\label{sec:app-monads} +\begin{figure}[h] +\begin{Verbatim} +module Cat.Category.Monad.Kleisli + {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + +record RawMonad : Set ℓ where + field + omap : Object → Object + pure : {X : Object} → ℂ [ X , omap X ] + bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ] + + fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ omap A , omap B ] + fmap f = bind (pure <<< f) + + _>=>_ : {A B C : Object} + → ℂ [ A , omap B ] → ℂ [ B , omap C ] → ℂ [ A , omap C ] + f >=> g = f >>> (bind g) + + join : {A : Object} → ℂ [ omap (omap A) , omap A ] + join = bind identity + + IsIdentity = {X : Object} + → bind pure ≡ identity {omap X} + IsNatural = {X Y : Object} (f : ℂ [ X , omap Y ]) + → pure >=> f ≡ f + IsDistributive = {X Y Z : Object} + (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ]) + → (bind f) >>> (bind g) ≡ bind (f >=> g) + +record IsMonad (raw : RawMonad) : Set ℓ where + open RawMonad raw public + field + isIdentity : IsIdentity + isNatural : IsNatural + isDistributive : IsDistributive +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category.Monad.Kleisli}. Definition of + Kleisli monads.} +\end{figure} +% +\begin{figure}[h] +\begin{Verbatim} +module Cat.Category.Monad.Monoidal + {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + +private + ℓ = ℓa ⊔ ℓb + +open Category ℂ using (Object ; Arrow ; identity ; _<<<_) + +record RawMonad : Set ℓ where + field + R : EndoFunctor ℂ + pureNT : NaturalTransformation Functors.identity R + joinNT : NaturalTransformation F[ R ∘ R ] R + + Romap = Functor.omap R + fmap = Functor.fmap R + + pureT : Transformation Functors.identity R + pureT = fst pureNT + + pure : {X : Object} → ℂ [ X , Romap X ] + pure = pureT _ + + pureN : Natural Functors.identity R pureT + pureN = snd pureNT + + joinT : Transformation F[ R ∘ R ] R + joinT = fst joinNT + join : {X : Object} → ℂ [ Romap (Romap X) , Romap X ] + join = joinT _ + joinN : Natural F[ R ∘ R ] R joinT + joinN = snd joinNT + + bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ] + bind {X} {Y} f = join <<< fmap f + + IsAssociative : Set _ + IsAssociative = {X : Object} + → joinT X <<< fmap join ≡ join <<< join + IsInverse : Set _ + IsInverse = {X : Object} + → join <<< pure ≡ identity {Romap X} + × join <<< fmap pure ≡ identity {Romap X} + +record IsMonad (raw : RawMonad) : Set ℓ where + open RawMonad raw public + field + isAssociative : IsAssociative + isInverse : IsInverse +\end{Verbatim} +\caption{Excerpt from module \texttt{Cat.Category.Monad.Monoidal}. Definition of + Monoidal monads.} +\end{figure}