cat/doc/sources.tex

430 lines
14 KiB
TeX
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

\chapter{Source code excerpts}
\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. 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}
\label{sec:app-cubical}
\begin{figure}[h]
\label{fig:path}
\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}
\clearpage
%
\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}