amelia
/
cubical


-- We begin by adding some primitive bindings using the PRIMITIVE pragma.

--

-- It goes like this: PRIMITIVE primName varName.

--

-- If the varName is dropped, then it's taken to be the same as primName.

--

-- If there is a previous declaration for the varName, then the type

-- is checked against the internally-known "proper" type for the primitive.


-- Universe of fibrant types

{-# PRIMITIVE Type #-}


-- Universe of non-fibrant types

{-# PRIMITIVE Pretype #-}


-- Fibrant is a fancy word for "has a composition structure". Most types

-- we inherit from MLTT are fibrant:

--

-- Stuff like products Π, sums Σ, naturals, booleans, lists, etc., all

-- have composition structures.

--

-- The non-fibrant types are part of the structure of cubical

-- categories: The interval, partial elements, cubical subtypes, ...


-- The interval

---------------


-- The interval has two endpoints i0 and i1.

-- These form a de Morgan algebra.

I : Pretype

{-# PRIMITIVE Interval I #-}


i0, i1 : I

{-# PRIMITIVE i0 #-}

{-# PRIMITIVE i1 #-}


-- "minimum" on the interval

iand : I -> I -> I

{-# PRIMITIVE iand #-}


-- "maximum" on the interval.

ior : I -> I -> I

{-# PRIMITIVE ior #-}


-- The interpretation of iand as min and ior as max justifies the fact that

-- ior i (inot i) != i1, since that equality only holds for the endpoints.


-- inot i = 1 - i is a de Morgan involution.

inot : I -> I

{-# PRIMITIVE inot #-}


-- Paths

--------


-- Since every function in type theory is internally continuous,

-- and the two endpoints i0 and i1 are equal, we can take the type of

-- equalities to be continuous functions out of the interval.

-- That is, x ≡ y iff. ∃ f : I -> A, f i0 = x, f i1 = y.


-- The type PathP generalises this to dependent products (i : I) -> A i.


PathP : (A : I -> Type) -> A i0 -> A i1 -> Type

{-# PRIMITIVE PathP #-}


-- By taking the first argument to be constant we get the equality type

-- Path.


Path : {A : Type} -> A -> A -> Type

Path {A} = PathP (\i -> A)


-- reflexivity is given by constant paths


refl : {A : Type} {x : A} -> Path x x

refl {A} {x} i = x


-- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that

-- sym p i0 = p (inot i0) = p i1

-- sym p i1 = p (inot i1) = p i0

-- This has the correct endpoints.


sym : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x

sym p i = p (inot i)


id : {A : Type} -> A -> A

id x = x


the : (A : Pretype) -> A -> A

the A x = x


-- The eliminator for the interval says that if you have x : A i0 and y : A i1,

-- and x ≡ y, then you can get a proof A i for every element of the interval.

iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i

iElim p i = p i


-- This corresponds to the elimination principle for the HIT

-- data I : Pretype where

-- i0 i1 : I

-- seg : i0 ≡ i1


-- The singleton subtype of A at x is the type of elements of y which

-- are equal to x.

Singl : (A : Type) -> A -> Type

Singl A x = (y : A) * Path x y


-- Contractible types are those for which there exists an element to which

-- all others are equal.

isContr : Type -> Type

isContr A = (x : A) * ((y : A) -> Path x y)


-- Using the connection \i j -> y.2 (iand i j), we can prove that

-- singletons are contracible. Together with transport later on,

-- we get the J elimination principle of paths.

singContr : {A : Type} {a : A} -> isContr (Singl A a)

singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))


-- Some more operations on paths. By rearranging parentheses we get a

-- proof that the images of equal elements are themselves equal.

cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)

cong f p i = f (p i)


-- These satisfy definitional equalities, like congComp and congId, which are

-- propositional in vanilla MLTT.

congComp : {A : Type} {B : Type} {C : Type}

 {f : A -> B} {g : B -> C} {x : A} {y : A}

 (p : Path x y)

 -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)

congComp p = refl


congId : {A : Type} {x : A} {y : A}

 (p : Path x y)

 -> Path (cong (id {A}) p) p

congId p = refl


-- Just like rearranging parentheses gives us cong, swapping the value

-- and interval binders gives us function extensionality.

funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 (h : (x : A) -> Path (f x) (g x))

 -> Path f g

funext h i x = h x i


-- The proposition associated with an element of the interval

-------------------------------------------------------------


Eq_s : {A : Pretype} -> A -> A -> Pretype

{-# PRIMITIVE Eq_s #-}


refl_s : {A : Pretype} {x : A} -> Eq_s x x

{-# PRIMITIVE refl_s #-}


J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p

{-# PRIMITIVE J_s #-}


K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p

{-# PRIMITIVE K_s #-}


-- Associated with every element i : I of the interval, we have the type

-- IsOne i which is inhabited only when i = i1. In the model, this

-- corresponds to the map [φ] from the interval cubical set to the

-- subobject classifier.


IsOne : I -> Pretype

IsOne i = Eq_s i i1


-- The value itIs1 witnesses the fact that i1 = i1.

itIs1 : IsOne i1

itIs1 = refl_s


-- Partial elements

-------------------

--

-- Since a function I -> A has two endpoints, and a function I -> I -> A

-- has four endpoints + four functions I -> A as "sides" (obtained by

-- varying argument while holding the other as a bound variable), we

-- refer to elements of I^n -> A as "cubes".


-- This justifies the existence of partial elements, which are, as the

-- name implies, partial cubes. Namely, a Partial φ A is an element of A

-- which depends on a proof that IsOne φ.


Partial : I -> Type -> Pretype

{-# PRIMITIVE Partial #-}


-- There is also a dependent version where the type A is itself a

-- partial element.


PartialP : (phi : I) -> Partial phi Type -> Pretype

{-# PRIMITIVE PartialP #-}


-- Why is Partial φ A not just defined as φ -> A? The difference is that

-- Partial φ A has an internal representation which definitionally relates

-- any two partial elements which "agree everywhere", that is, have

-- equivalent values for every possible assignment of variables which

-- makes IsOne φ hold.


-- Cubical Subtypes

--------------------


-- Given A : Type, phi : I, and a partial element u : A defined on φ,

-- we have the type Sub A phi u, notated A[phi -> u] in the output of

-- the type checker, whose elements are "extensions" of u.


-- That is, element of A[phi -> u] is an element of A defined everywhere

-- (a total element), which, when IsOne φ, agrees with u.


Sub : (A : Type) (phi : I) -> Partial phi A -> Pretype

{-# PRIMITIVE Sub #-}


-- Every total element u : A can be made partial on φ by ignoring the

-- constraint. Furthermore, this "totally partial" element agrees with

-- the original total element on φ.

inS : {A : Type} {phi : I} (u : A) -> Sub A phi (\x -> u)

{-# PRIMITIVE inS #-}


-- When IsOne φ, outS {A} {φ} {u} x reduces to u itIs1.

-- This implements the fact that x agrees with u on φ.

outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A

{-# PRIMITIVE outS #-}


-- The composition operation

----------------------------


-- Now that we have syntax for specifying partial cubes,

-- and specifying that an element agrees with a partial cube,

-- we can describe the composition operation.


primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> Sub (A i1) phi (u i1)

{-# PRIMITIVE comp primComp #-}


comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1

comp A {phi} u a0 = outS (primComp A {phi} u a0)


-- In particular, when φ is a disjunction of the form

-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a

-- "tube", an open square with no floor or roof:

--

-- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,

-- we draw:

--

-- x q i1

-- | |

-- \j -> x | | \j -> q j

-- | |

-- x q i0

--

-- The composition operation says that, as long as we can provide a

-- "floor" connecting x -- q i0, as a total element of A which, on

-- phi, extends u i0, then we get the "roof" connecting x and q i1

-- for free.

--

-- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the

-- "floor", and composition gets us the dotted line:

--

-- x..........z

-- | |

-- x | | q j

-- | |

-- x----------y

-- p i


trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z

trans {A} {x} p q i =

 comp (\i -> A)

 {ior i (inot i)}

 (\j [ (i = i0) -> x, (i = i1) -> q j ])

 (inS (p i))


-- In particular when the formula φ = i0 we get the "opposite face" to a

-- single point, which corresponds to transport.


transp : (A : I -> Type) (x : A i0) -> A i1

transp A x = comp A {i0} (\i [ ]) (inS x)


-- Since we have the iand operator, we can also derive the *filler* of a cube,

-- which connects the given face and the output of composition.


fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) (a0 : Sub (A i0) phi (u i0)) -> PathP A (outS a0) (comp A {phi} u a0)

fill A {phi} u a0 i =

 comp (\j -> A (iand i j))

 {ior phi (inot i)}

 (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])

 (inS (outS a0))


hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A

hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0


hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> Path (outS a0) (hcomp u a0)

hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i


-- For instance, the filler of the previous composition square

-- tells us that trans p refl = p:


transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p

transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)


rightCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p (sym p)) refl

rightCancel p j i = cube p i1 j i where

 cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A

 cube {A} {x} p k j i =

 hfill {A} (\ k [ (i = i0) -> x

 , (i = i1) -> p (iand (inot k) (inot j))

 , (j = i1) -> x

 ])

 (inS (p (iand i (inot j)))) k


leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl

leftCancel p = rightCancel (sym p)


transpFill : {A : I -> Type} (x : A i0) -> PathP A x (transp (\i -> A i) x)

transpFill {A} x i = fill (\i -> A i) (\k []) (inS x) i


-- Reduction of composition

---------------------------

--

-- Composition reduces on the structure of the family A : I -> Type to create

-- the element a1 : (A i1)[phi -> u i1].

--

-- For instance, when filling a cube of functions, the behaviour is to

-- first transport backwards along the domain, apply the function, then

-- forwards along the codomain.


transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path C D)

 -> (f : A -> C) -> Path (transp (\i -> p i -> q i) f)

 (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))

transpFun p q f = refl


transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}

 -> (f : (x : A i0) -> B i0 x)

 -> Path (transp (\i -> (x : A i) -> B i x) f)

 (\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i)))

 (f (fill (\j -> A (inot j)) (\k []) (inS x) i1)))

transpDFun f = refl


-- When considering the more general case of a composition respecing sides,

-- the outer transport becomes a composition.


-- Glueing and Univalence

-------------------------


-- First, let's get some definitions out of the way.

--

-- The *fiber* of a function f : A -> B at a point y : B is the type of

-- inputs x : A which f takes to y, that is, for which there exists a

-- path f(x) = y.


fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type

fiber f y = (x : A) * Path y (f x)


-- An *equivalence* is a function where every fiber is contractible.

-- That is, for every point in the codomain y : B, there is exactly one

-- point in the input which f maps to y.


isEquiv : {A : Type} {B : Type} -> (A -> B) -> Type

isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)


-- By extracting this point, which must exist because the fiber is contractible,

-- we can get an inverse of f:


invert : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A

invert eqv y = (eqv y) .1 .1


retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type

retract {A} {B} f g = (a : A) -> Path (g (f a)) a


contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A

contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))


-- Proving that it's also a retraction is left as an exercise to the

-- reader. We can package together a function and a proof that it's an

-- equivalence to get a capital-E Equivalence.


Equiv : (A : Type) (B : Type) -> Type

Equiv A B = (f : A -> B) * isEquiv {A} {B} f


-- The identity function is an equivalence between any type A and

-- itself.

idEquiv : {A : Type} -> isEquiv (id {A})

idEquiv y = ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))


-- The glue operation expresses that "extensibility is invariant under

-- equivalence". Less concisely, the Glue type and its constructor,

-- glue, let us extend a partial element of a partial type to a total

-- element of a total type, by "gluing" the partial type T using a

-- partial equivalence e onto a total type A.


-- In particular, we have that when φ = i1, Glue A [i1 -> (T, f)] = T.


primGlue : (A : Type) {phi : I}

 (T : Partial phi Type)

 (e : PartialP phi (\o -> Equiv (T o) A))

 -> Type

{-# PRIMITIVE Glue primGlue #-}


-- The glue constructor extends the partial element t : T to a total

-- element of Glue A [φ -> (T, e)] as long as we have a total im : A

-- which is the image of f(t).

--

-- Agreeing with the condition that Glue A [i1 -> (T, e)] = T,

-- we have that glue {A} {i1} t im => t.

prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}

 -> (t : PartialP phi T)

 -> (im : Sub A phi (\o -> (e o).1 (t o)))

 -> primGlue A T e


{-# PRIMITIVE glue prim'glue #-}


glue : {A : Type} {phi : I} {Te : Partial phi ((T : Type) * Equiv T A)}

 -> (t : PartialP phi (\o -> (Te o).1))

 -> (im : Sub A phi (\o -> (Te o).2.1 (t o)))

 -> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2)

glue {A} {phi} {Te} t im = prim'glue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} t im


-- The unglue operation undoes a glueing. Since when φ = i1,

-- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ...

-- will have type T, and so to get back an A we need to apply the

-- partial equivalence f (defined everywhere).


primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)}

 -> primGlue A {phi} T e -> A


{-# PRIMITIVE unglue primUnglue #-}


unglue : {A : Type} (phi : I) {Te : Partial phi ((T : Type) * Equiv T A)}

 -> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2) -> A

unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2}


-- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn

-- as giving us the dotted line in:

--

-- T i0 ......... T i1

-- | |

-- | |

-- e i0 |~ ~| e i1

-- | |

-- | |

-- A i0 --------- A i1

-- A

--

-- Where the the two "e" sides are equivalences, and the Bottom side is

-- the line i : I |- A.

--

-- Thus, by choosing a base type, a set of partial types and partial

-- equivalences, we can make a line between two types (T i0) and (T i1).


Glue : (A : Type) {phi : I} -> Partial phi ((X : Type) * Equiv X A) -> Type

Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2)


-- For example, we can glue together the type A and the type B as long

-- as there exists an Equiv A B.

--

-- A ............ B

-- | |

-- | |

-- equiv |~ ua equiv ~| idEquiv {B}

-- | |

-- | |

-- B ------------ B

-- \i → B

--

univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B

univalence {A} {B} equiv i =

 Glue B (\[ (i = i0) -> (A, equiv),

 (i = i1) -> (B, the B, idEquiv {B}) ])


lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)

{-# PRIMITIVE lineToEquiv #-}


idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B

idToEquiv p = lineToEquiv (\i -> p i)


-- The fact that this diagram has 2 filled-in B sides explains the

-- complication in the proof below.

--

-- In particular, the actual behaviour of transp (\i -> univalence f i)

-- (x : A) is not just to apply f x to get a B (the left side), it also

-- needs to:

--

-- * For the Bottom side, compose along (\i -> B) (the Bottom side)

-- * For the right side, apply the inverse of the identity, which

-- is just identity, to get *some* b : B

--

-- But that b : B might not agree with the sides of the composition

-- operation in a more general case, so it composes along (\i -> B)

-- *again*!

--

-- Thus the proof: a simple cubical argument suffices, since

-- for any composition, its filler connects either endpoints. So

-- we need to come up with a filler for the Bottom and right faces.


univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1

univalenceBeta {A} {B} f i a =

 let

 -- The Bottom left corner

 botLeft : B

 botLeft = transp (\i -> B) (f.1 a)


 -- The "Bottom face" filler connects the Bottom-left corner, f.1 a,

 -- and the Bottom-right corner, which is the transport of f.1 a

 -- along \i -> B.

 botFace : Path (f.1 a) botLeft

 botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i


 -- The "right face" filler connects the Bottom-right corner and the

 -- upper-right corner, which is again a simple transport along

 -- \i -> B.

 rightFace : Path (transp (\i -> B) botLeft) botLeft

 rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)


 -- The goal is a path between the Bottom-left and top-right corners,

 -- which we can get by composing (in the path sense) the Bottom and

 -- right faces.

 goal : Path (transp (\i -> B) botLeft) (f.1 a)

 goal = trans rightFace (\i -> botFace (inot i))

 in goal i


-- The terms univalence + univalenceBeta suffice to prove the "full"

-- univalence axiom of Voevodsky, as can be seen in the paper

--

-- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.

--

-- Available freely here: https://arxiv.org/abs/1712.04890v3


J : {A : Type} {x : A}

 (P : (y : A) -> Path x y -> Type)

 (d : P x (\i -> x))

 {y : A} (p : Path x y)

 -> P y p

J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d


Jay : {A : Type} {x : A}

 (P : ((y : A) * Path x y) -> Type)

 (d : P (x, refl))

 (s : (y : A) * Path x y)

 -> P s

Jay P d s = transp (\i -> P ((singContr {A} {x}).2 s i)) d


-- Isomorphisms

---------------

--

-- Since isomorphisms are a much more convenient notion of equivalence

-- than contractible fibers, it's natural to ask why the CCHM paper, and

-- this implementation following that, decided on the latter for our

-- definition of equivalence.


isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type

isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x)


-- The reason is that the family of types IsIso is not a proposition!

-- This means that there can be more than one way for a function to be

-- an equivalence. This is Lemma 4.1.1 of the HoTT book.


Iso : Type -> Type -> Type

Iso A B = (f : A -> B) * isIso f


-- Nevertheless, we can prove that any function with an isomorphism

-- structure has contractible fibers, using a cubical argument adapted

-- from CCHM's implementation of cubical type theory:

--

-- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55


IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B

IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where

 f = iso.1

 g = iso.2.1

 s = iso.2.2.1

 t = iso.2.2.2


 lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path y (f x0)) (p1 : Path y (f x1))

 -> PathP (\i -> fiber f y) (x0, p0) (x1, p1)

 lemIso y x0 x1 p0 p1 =

 let

 rem0 : Path x0 (g y)

 rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 (inot i))))


 rem1 : Path x1 (g y)

 rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i))))


 p : Path x0 x1

 p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))


 fill0 : I -> I -> A

 fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k)

 , (i = i1) -> g y

 , (j = i0) -> g (p0 (inot i))

 ])

 (inS (g (p0 (inot i))))


 fill1 : I -> I -> A

 fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k)

 , (i = i1) -> g y

 , (j = i0) -> g (p1 (inot i)) ])

 (inS (g (p1 (inot i))))


 fill2 : I -> I -> A

 fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k))

 , (i = i1) -> rem1 (ior j (inot k))

 , (j = i1) -> g y ])

 (inS (g y))


 sq : I -> I -> A

 sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k)

 , (i = i1) -> fill1 j (inot k)

 , (j = i1) -> g y

 , (j = i0) -> t (p i) (inot k) ])

 (inS (fill2 i j))


 sq1 : I -> I -> B

 sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 (inot j)) k

 , (i = i1) -> s (p1 (inot j)) k

 , (j = i0) -> s (f (p i)) k

 , (j = i1) -> s y k

 ])

 (inS (f (sq i j)))

 in \i -> (p i, \j -> sq1 i (inot j))


 fCenter : (y : B) -> fiber f y

 fCenter y = (g y, sym (s y))


 fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w

 fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2


IsoToId : {A : Type} {B : Type} -> Iso A B -> Path A B

IsoToId i = univalence (IsoToEquiv i)


-- We can prove that any involutive function is an isomorphism, since

-- such a function is its own inverse.


involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f

involToIso {A} f inv = (f, inv, inv)


-- An example of univalence

---------------------------

--

-- The classic example of univalence is the equivalence

-- not : Bool \simeq Bool.

--

-- We define it here.


data Bool : Type where

 true : Bool

 false : Bool


not : Bool -> Bool

not = \case

 true -> false

 false -> true


elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b

elimBool P x y = \case

 true -> x

 false -> y


if : {A : Type} -> A -> A -> Bool -> A

if x y = \case

 true -> x

 false -> y


-- By pattern matching it suffices to prove (not (not true)) ≡ true and

-- not (not false) ≡ false. Since not (not true) computes to true (resp.

-- false), both proofs go through by refl.

notInvol : (x : Bool) -> Path (not (not x)) x

notInvol = elimBool (\b -> Path (not (not b)) b) refl refl


notp : Path Bool Bool

notp = univalence (IsoToEquiv (not, involToIso not notInvol))


-- This path actually serves to prove a simple lemma about the universes

-- of HoTT, namely, that any univalent universe is not a 0-type. If we

-- had HITs, we could prove that this fact holds for any n, but for now,

-- proving it's not an h-set is the furthest we can go.


-- First we define what it means for something to be false. In type theory,

-- we take ¬P = P → ⊥, where the Bottom type is the only type satisfying

-- the elimination principle

--

-- elimBottom : (P : Bottom -> Type) -> (b : Bottom) -> P b

--

-- This follows from setting Bottom := ∀ A, A.


data Bottom : Type where {}


elimBottom : (P : Bottom -> Pretype) -> (b : Bottom) -> P b

elimBottom P = \case {}


absurd : {P : Pretype} -> Bottom -> P

absurd = \case {}


-- We prove that true != false by transporting along the path

--

-- \i -> if (Bool -> Bool) A (p i)

-- (Bool -> Bool) ------------------------------------ A

--

-- To verify that this has the correct endpoints, check out the endpoints

-- for p:

--

-- true ------------------------------------ false

--

-- and evaluate the if at either end.


trueNotFalse : Path true false -> Bottom

trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id


-- To be an h-Set is to have no "higher path information". Alternatively,

--

-- isHSet A = (x : A) (y : A) -> isHProp (Path x y)

--


isProp : Type -> Type

isProp A = (x : A) (y : A) -> Path x y


isHSet : Type -> Type

isHSet A = (x : A) (y : A) -> isProp (Path x y)


-- We can prove *a* contradiction (note: this is a direct proof!) by adversarially

-- choosing two paths p, q that we know are not equal. Since "equal" paths have

-- equal behaviour when transporting, we can choose two paths p, q and a point x

-- such that transporting x along p gives a different result from x along q.

--

-- Since transp notp = not but transp refl = id, that's what we go with. The choice

-- of false as the point x is just from the endpoints of trueNotFalse.


universeNotSet : isHSet Type -> Bottom

universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl i j) false)


-- Funext is an inverse of happly

---------------------------------

--

-- Above we proved function extensionality, namely, that functions

-- pointwise equal everywhere are themselves equal.

-- However, this formulation of the axiom is known as "weak" function

-- extensionality. The strong version is as follows:


Hom : {A : Type} {B : A -> Type} (f : (x : A) -> B x) -> (g : (x : A) -> B x) -> Type

Hom {A} f g = (x : A) -> Path (f x) (g x)


happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 -> (p : Path f g) -> Hom f g

happly p x i = p i x


-- Strong function extensionality: happly is an equivalence.


happlyIsIso : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 -> isIso {Path f g} {Hom f g} happly

happlyIsIso {A} {B} {f} {g} = (funext {A} {B} {f} {g}, \hom -> refl, \path -> refl)


pathIsHom : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}

 -> Path (Path f g) (Hom f g)

pathIsHom {A} {B} {f} {g} =

 let

 theIso : Iso (Path f g) (Hom f g)

 theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})

 in univalence (IsoToEquiv theIso)


-- Inductive types

-------------------

--

-- An inductive type is a type freely generated by a finite set of

-- constructors. For instance, the type of natural numbers is generated

-- by the constructors for "zero" and "successor".


data Nat : Type where

 zero : Nat

 succ : Nat -> Nat


-- Pattern matching allows us to prove that these initial types are

-- initial algebras for their corresponding functors.


Nat_elim : (P : Nat -> Type) -> P zero -> ((x : Nat) -> P x -> P (succ x)) -> (x : Nat) -> P x

Nat_elim P pz ps = \case

 zero -> pz

 succ x -> ps x (Nat_elim P pz ps x)


zeroNotSucc : {x : Nat} -> Path zero (succ x) -> Bottom

zeroNotSucc p = transp (\i -> fun (p i)) (p i0) where

 fun : Nat -> Type

 fun = \case

 zero -> Nat

 succ x -> Bottom


succInj : {x : Nat} {y : Nat} -> Path (succ x) (succ y) -> Path x y

succInj p i = pred (p i) where

 pred : Nat -> Nat

 pred = \case

 zero -> zero

 succ x -> x


-- The type of integers can be defined as A + B, where "pos n" means +n

-- and "neg n" means -(n + 1).


data Int : Type where

 pos : Nat -> Int

 neg : Nat -> Int


-- On this representation we can define the successor and predecessor

-- functions by (nested) induction.


sucZ : Int -> Int

sucZ = \case

 pos n -> pos (succ n)

 neg n ->

 let suc_neg : Nat -> Int

 suc_neg = \case

 zero -> pos zero

 succ n -> neg n

 in suc_neg n


predZ : Int -> Int

predZ = \case

 pos n ->

 let pred_pos : Nat -> Int

 pred_pos = \case

 zero -> neg zero

 succ n -> pos n

 in pred_pos n

 neg n -> neg (succ n)


-- And prove that the successor function is an isomorphism, and thus, an

-- equivalence.


sucEquiv : isIso sucZ

sucEquiv =

 let

 sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x

 sucPredZ = \case

 pos n ->

 let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)

 k = \case

 zero -> refl

 succ n -> refl

 in k n

 neg n -> refl

 predSucZ : (x : Int) -> Path (predZ (sucZ x)) x

 predSucZ = \case

 pos n -> refl

 neg n ->

 let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)

 k = \case

 zero -> refl

 succ n -> refl

 in k n

 in (predZ, sucPredZ, predSucZ)


-- Univalence gives us a path between integers such that transp intPath

-- x = suc x, transp (sym intPath) x = pred x


intPath : Path Int Int

intPath = univalence (IsoToEquiv (sucZ, sucEquiv))


-- Higher inductive types

-------------------------

--

-- While inductive types let us generate discrete spaces like the

-- naturals or integers, they do not support defining higher-dimensional

-- structures given by spaces with points and paths.


-- A very simple higher inductive type is the interval, given by


data Interval : Type where

 ii0 : Interval

 ii1 : Interval

 seg i : Interval [ (i = i0) -> ii0, (i = i1) -> ii1 ]


-- This expresses that we have two points ii0 and ii1 and a path (\i ->

-- seg i) with endpoints ii0 and ii1.


-- With this type we can reproduce the proof of Lemma 6.3.2 from the

-- HoTT book:


iFunext : {A : Type} {B : A -> Type} (f : (x : A) -> B x) (g : (x : A) -> B x)

 -> ((x : A) -> Path (f x) (g x)) -> Path f g

iFunext f g p i = h' (seg i) where

 h : (x : A) -> Interval -> B x

 h x = \case

 ii0 -> f x

 ii1 -> g x

 seg i -> p x i


 h' : Interval -> (x : A) -> B x

 h' i x = h x i


-- Of course, Cubical Type Theory also has an interval (pre)type, but

-- that, unlike the Interval here, is not Kan: it has no composition

-- structure.


-- Another simple higher-inductive type is the circle, with a point and

-- a non-trivial loop, (\i -> loop i).


data S1 : Type where

 base : S1

 loop i : S1 [ (i = i1) -> base, (i = i0) -> base ]


-- By writing a function from the circle to the universe of types Type,

-- we can calculate winding numbers along the circle.


helix : S1 -> Type

helix = \case

 base -> Int

 loop i -> intPath i


loopP : Path base base

loopP i = loop i


winding : Path base base -> Int

winding p = transp (\i -> helix (p i)) (pos zero)


-- For instance, going around the loop once has a winding number of +1,


windingLoop : Path (winding (\i -> loop i)) (pos (succ zero))

windingLoop = refl


-- Going backwards has a winding number of -1 (remember the

-- representation of integers),


windingSymLoop : Path (winding (\i -> loop (inot i))) (neg zero)

windingSymLoop = refl


-- And going around the trivial loop (\i -> base) goes around the the

-- non-trivial loop (\i -> loop) zero times.


windingBase : Path (winding (\i -> base)) (pos zero)

windingBase = refl


goAround : Int -> Path base base

goAround =

 \case

 pos n -> forwards n

 neg n -> backwards n

 where

 forwards : Nat -> Path base base

 forwards = \case

 zero -> refl

 succ n -> trans (forwards n) (\i -> loop i)

 backwards : Nat -> Path base base

 backwards = \case

 zero -> \i -> loop (inot i)

 succ n -> trans (backwards n) (\i -> loop (inot i))


-- One particularly general higher inductive type is the homotopy pushout,

-- which can be seen as a kind of sum B + C with the extra condition that

-- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.


data Pushout {A : Type} {B : Type} {C : Type} (f : A -> B) (g : A -> C) : Type where

 inl : (x : B) -> Pushout f g

 inr : (y : C) -> Pushout f g

 push i : (a : A) -> Pushout f g [ (i = i0) -> inl (f a), (i = i1) -> inr (g a) ]


-- The name is due to the category-theoretical notion of pushout.

-- TODO: finish writing this tomorrow lol


data Susp (A : Type) : Type where

 north : Susp A

 south : Susp A

 merid i : A -> Susp A [ (i = i0) -> north, (i = i1) -> south ]


data Unit : Type where

 tt : Unit


unitEta : (x : Unit) -> Path x tt

unitEta = \case tt -> refl


unitContr : isContr Unit

unitContr = (tt, \x -> sym (unitEta x))


poSusp : Type -> Type

poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)


Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)

Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where

 poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A

 poSusp_to_Susp = \case

 inl x -> north

 inr x -> south

 push x i -> merid x i


 Susp_to_poSusp : {A : Type} -> Susp A -> poSusp A

 Susp_to_poSusp = \case

 north -> inl tt

 south -> inr tt

 merid x i -> push x i


 Susp_to_poSusp_to_Susp : {A : Type} -> (x : Susp A) -> Path (poSusp_to_Susp (Susp_to_poSusp x)) x

 Susp_to_poSusp_to_Susp = \case

 north -> refl

 south -> refl

 merid x i -> refl


 poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x

 poSusp_to_Susp_to_poSusp {A} = \case

 inl x -> cong inl (sym (unitEta x))

 inr x -> cong inr (sym (unitEta x))

 push x i -> refl


data T2 : Type where

 baseT : T2

 pathOne i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]

 pathTwo i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]

 square i j : T2 [

 (j = i0) -> pathTwo i,

 (j = i1) -> pathTwo i,

 (i = i0) -> pathOne j,

 (i = i1) -> pathOne j

 ]


TorusIsTwoCircles : Path T2 (S1 * S1)

TorusIsTwoCircles = univalence (IsoToEquiv theIso) where

 torusToCircs : T2 -> S1 * S1

 torusToCircs = \case

 baseT -> (base, base)

 pathOne i -> (loop i, base)

 pathTwo i -> (base, loop i)

 square i j -> (loop i, loop j)


 circsToTorus : (S1 * S1) -> T2

 circsToTorus pair = go pair.1 pair.2

 where

 baseCase : S1 -> T2

 baseCase = \case

 base -> baseT

 loop j -> pathTwo j


 loopCase : Path baseCase baseCase

 loopCase i = \case

 base -> pathOne i

 loop j -> square i j


 go : S1 -> S1 -> T2

 go = \case

 base -> baseCase

 loop i -> loopCase i


 torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x

 torusToCircsToTorus = \case

 baseT -> refl

 pathOne i -> refl

 pathTwo i -> refl

 square i j -> refl


 circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p

 circsToTorusToCircs pair = go pair.1 pair.2 where

 baseCase : (y : S1) -> Path (torusToCircs (circsToTorus (base, y))) (base, y)

 baseCase = \case

 base -> refl

 loop j -> refl


 loopCase : (i : I) (y : S1) -> Path (torusToCircs (circsToTorus (loop i, y))) (loop i, y )

 loopCase i = \case

 base -> refl

 loop j -> refl


 go : (x : S1) (y : S1) -> Path (torusToCircs (circsToTorus (x, y))) (x, y)

 go = \case

 base -> baseCase

 loop i -> loopCase i


 theIso : Iso T2 (S1 * S1)

 theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)


abs : Int -> Nat

abs = \case

 pos n -> n

 neg n -> succ n


sign : Int -> Bool

sign = \case

 pos n -> true

 neg n -> false


boolAnd : Bool -> Bool -> Bool

boolAnd = \case

 true -> \case

 true -> true

 false -> false

 false -> \case

 true -> false

 false -> false


plusNat : Nat -> Nat -> Nat

plusNat = \case

 zero -> \x -> x

 succ n -> \x -> succ (plusNat n x)


plusZero : (x : Nat) -> Path (plusNat zero x) x

plusZero = \case

 zero -> refl

 succ n -> \i -> succ (plusZero n i)


multNat : Nat -> Nat -> Nat

multNat = \case

 zero -> \x -> zero

 succ n -> \x -> plusNat x (multNat n x)


multInt : Int -> Int -> Int

multInt x y = signify (multNat (abs x) (abs y)) (boolAnd (sign x) (sign y)) where

 signify : Nat -> Bool -> Int

 signify = \case

 zero -> \x -> pos zero

 succ n -> \case

 true -> pos (succ n)

 false -> neg n


two : Int

two = pos (succ (succ zero))


four : Int

four = multInt two two


sixteen : Int

sixteen = multInt four four


Prop : Type

Prop = (A : Type) * isProp A


data Sq (A : Type) : Type where

 inc : A -> Sq A

 sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ]


isProp_isSet : {A : Type} -> isProp A -> isHSet A

isProp_isSet h a b p q j i =

 hcomp {A}

 (\k [ (i = i0) -> h a a k

 , (i = i1) -> h a b k

 , (j = i0) -> h a (p i) k

 , (j = i1) -> h a (q i) k

 ])

 (inS a)


isProp_isProp : {A : Type} -> isProp (isProp A)

isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i


Sq_rec : {A : Type} {B : Type}

 -> isProp B

 -> (f : A -> B)

 -> Sq A -> B

Sq_rec prop f =

 \case

 inc x -> f x

 sq x y i -> prop (work x) (work y) i

 where

 work : Sq A -> B

 work = \case

 inc x -> f x


hitTranspExample : Path (inc false) (inc true)

hitTranspExample i = transp (\i -> Sq (notp i)) (sq (inc true) (inc false) i)


data S2 : Type where

 base2 : S2

 surf2 i j : S2 [ (i = i0) -> base2, (i = i1) -> base2, (j = i0) -> base2, (j = i1) -> base2]


S2IsSuspS1 : Path S2 (Susp S1)

S2IsSuspS1 = univalence (IsoToEquiv iso) where

 toS2 : Susp S1 -> S2

 toS2 = \case { north -> base2; south -> base2; merid x i -> sphMerid x i } where

 sphMerid = \case

 base -> \i -> base2

 loop j -> \i -> surf2 i j


 suspSurf : I -> I -> I -> Susp S1

 suspSurf i j = hfill {Susp S1} (\k [ (i = i0) -> north

 , (i = i1) -> merid base (inot k)

 , (j = i0) -> merid base (iand (inot k) i)

 , (j = i1) -> merid base (iand (inot k) i)

 ])

 (inS (merid (loop j) i))


 fromS2 : S2 -> Susp S1

 fromS2 = \case { base2 -> north; surf2 i j -> suspSurf i j i1 }


 toFromS2 : (x : S2) -> Path (toS2 (fromS2 x)) x

 toFromS2 = \case { base2 -> refl; surf2 i j -> \k -> toS2 (suspSurf i j (inot k)) }


 fromToS2 : (x : Susp S1) -> Path (fromS2 (toS2 x)) x

 fromToS2 = \case { north -> refl; south -> \i -> merid base i; merid x i -> meridCase i x } where

 meridCase : (i : I) (x : S1) -> Path (fromS2 (toS2 (merid x i))) (merid x i)

 meridCase i = \case

 base -> \k -> merid base (iand i k)

 loop j -> \k -> suspSurf i j (inot k)


 iso : Iso S2 (Susp S1)

 iso = (fromS2, toS2, fromToS2, toFromS2)


data S3 : Type where

 base3 : S3

 surf3 i j k : S3 [ (i = i0) -> base3, (i = i1) -> base3, (j = i0) -> base3, (j = i1) -> base3, (k = i0) -> base3, (k = i1) -> base3 ]


S3IsSuspS2 : Path S3 (Susp S2)

S3IsSuspS2 = univalence (IsoToEquiv iso) where

 toS3 : Susp S2 -> S3

 toS3 = \case { north -> base3; south -> base3; merid x i -> sphMerid x i } where

 sphMerid = \case

 base2 -> \i -> base3

 surf2 j k -> \i -> surf3 i j k


 suspSurf : I -> I -> I -> I -> Susp S2

 suspSurf i j k = hfill {Susp S2} (\l [ (i = i0) -> north

 , (i = i1) -> merid base2 (inot l)

 , (j = i0) -> merid base2 (iand (inot l) i)

 , (j = i1) -> merid base2 (iand (inot l) i)

 , (k = i0) -> merid base2 (iand (inot l) i)

 , (k = i1) -> merid base2 (iand (inot l) i)

 ])

 (inS (merid (surf2 j k) i))


 fromS3 : S3 -> Susp S2

 fromS3 = \case { base3 -> north; surf3 i j k -> suspSurf i j k i1 }


 toFromS3 : (x : S3) -> Path (toS3 (fromS3 x)) x

 toFromS3 = \case { base3 -> refl; surf3 i j k -> \l -> toS3 (suspSurf i j k (inot l)) }


 fromToS3 : (x : Susp S2) -> Path (fromS3 (toS3 x)) x

 fromToS3 = \case { north -> refl; south -> \i -> merid base2 i; merid x i -> meridCase i x } where

 meridCase : (i : I) (x : S2) -> Path (fromS3 (toS3 (merid x i))) (merid x i)

 meridCase i = \case

 base2 -> \k -> merid base2 (iand i k)

 surf2 j k -> \l -> suspSurf i j k (inot l)


 iso : Iso S3 (Susp S2)

 iso = (fromS3, toS3, fromToS3, toFromS3)


ap_s : {A : Pretype} {B : Pretype} (f : A -> B) {x : A} {y : A} -> Eq_s x y -> Eq_s (f x) (f y)

ap_s {A} {B} f {x} {y} = J_s (\y p -> Eq_s (f x) (f y)) refl_s


subst_s : {A : Pretype} (P : A -> Pretype) {x : A} {y : A} -> Eq_s x y -> P x -> P y

subst_s {A} P {x} {z} p px = J_s {A} {x} (\y p -> P x -> P y) id p px


sym_s : {A : Pretype} {x : A} {y : A} -> Eq_s x y -> Eq_s y x

sym_s {A} {x} {y} = J_s {A} {x} (\y p -> Eq_s y x) refl_s


UIP : {A : Pretype} {x : A} {y : A} (p : Eq_s x y) (q : Eq_s x y) -> Eq_s p q

UIP {A} {x} {y} p q = J_s (\y p -> (q : Eq_s x y) -> Eq_s p q) (uipRefl A x) p q where

 uipRefl : (A : Pretype) (x : A) (p : Eq_s x x) -> Eq_s refl_s p

 uipRefl A x p = K_s {A} {x} (\q -> Eq_s refl_s q) refl_s p


strictEq_pathEq : {A : Type} {x : A} {y : A} -> Eq_s x y -> Path x y

strictEq_pathEq {A} {x} {y} eq = J_s {A} {x} (\y p -> Path x y) (\i -> x) {y} eq


seq_pathRefl : {A : Type} {x : A} (p : Eq_s x x) -> Eq_s (strictEq_pathEq p) (refl {A} {x})

seq_pathRefl {A} {x} p = K_s (\p -> Eq_s (strictEq_pathEq {A} {x} {x} p) (refl {A} {x})) refl_s p


Path_nat_strict_nat : (x : Nat) (y : Nat) -> Path x y -> Eq_s x y

Path_nat_strict_nat = \case { zero -> zeroCase; succ x -> succCase x } where

 zeroCase : (y : Nat) -> Path zero y -> Eq_s zero y

 zeroCase = \case

 zero -> \p -> refl_s

 succ x -> \p -> absurd (zeroNotSucc p)

 succCase : (x : Nat) (y : Nat) -> Path (succ x) y -> Eq_s (succ x) y

 succCase x = \case

 zero -> \p -> absurd (zeroNotSucc (sym p))

 succ y -> \p -> ap_s succ (Path_nat_strict_nat x y (succInj p))


pathToEqS_K : {A : Type} {x : A}

 -> (s : {x : A} {y : A} -> Path x y -> Eq_s x y)

 -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p

pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop where

 psloop : P (strictEq_pathEq (p_to_s loop))

 psloop = K_s (\l -> P (strictEq_pathEq {A} {x} {x} l)) pr (p_to_s {x} {x} loop)


 inv : (y : A) (l : Path x y) -> Path (strictEq_pathEq (p_to_s l)) l

 inv y l = J {A} {x} (\y l -> Path (strictEq_pathEq (p_to_s l)) l) (strictEq_pathEq aux) {y} l where

 aux : Eq_s (strictEq_pathEq (p_to_s (\i -> x))) (\i -> x)

 aux = seq_pathRefl (p_to_s (\i -> x))


pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isHSet A

pathToEq_isSet {A} p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where

 axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isHSet A

 axK_to_isSet K x y p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where

 uipRefl : (x : A) (p : Path x x) -> Path refl p

 uipRefl x p = K {x} (\q -> Path refl q) refl p


Nat_isSet : isHSet Nat

Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)


equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y

equivCtr e y = (e.2 y).1


equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)

 -> (v : fiber e.1 y) -> Path (equivCtr e y) v

equivCtrPath e y = (e.2 y).2


contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u

contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) as c -> p.2 (u c) i ]) (inS p.1)


contr' : {A : Type} -> ({phi : I} -> (u : Partial phi A) -> Sub A phi u) -> isContr A

contr' {A} contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where

 x : A

 x = outS (contr (\ []))


leftIsOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s (ior a b) i1

leftIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior i b)) refl_s (sym_s p)


rightIsOne : {a : I} {b : I} -> Eq_s b i1 -> Eq_s (ior a b) i1

rightIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p)


bothAreOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s b i1 -> Eq_s (iand a b) i1

bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)


test : {X : Type} -> (S1 -> X) -> (a : X) * Path a a

test {X} f = (f base, \i -> f (loop i))


test' : {X : Type} -> ((a : X) * Path a a) -> S1 -> X

test' {X} p = \case

 base -> p.1

 loop i -> p.2 i


test_test' : {X : Type} -> (f : S1 -> X) -> Path (test' (test f)) f

test_test' {X} f = funext {S1} {\s -> X} {\x -> test' (test f) x} {f} h where

 h : (x : S1) -> Path (test' (test f) x) (f x)

 h = \case

 base -> refl

 loop i -> refl


test'_test : {X : Type} -> (x : (a : X) * Path a a) -> Path (test (test' x)) x

test'_test x = refl


test'' : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a)

test'' = IsoToId {S1 -> X} {(a : X) * Path a a} (test, test', test'_test, test_test')


-- HoTT book lemma 8.9.1

encodeDecode : {A : Type} {a0 : A}

 -> (code : A -> Type)

 -> (c0 : code a0)

 -> (decode : (x : A) -> code x -> (Path a0 x))

 -> ((c : code a0) -> Path (transp (\i -> code (decode a0 c i)) c0) c)

 -> Path (decode a0 c0) refl

 -> Path (Path a0 a0) (code a0)

encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode a0, encDec, decEnc) where

 encode : {x : A} -> Path a0 x -> code x

 encode alpha = transp (\i -> code (alpha i)) c0


 encodeRefl : Path (encode refl) c0

 encodeRefl = sym (transpFill {\i -> code a0} c0)


 decEnc : {x : A} (p : Path a0 x) -> Path (decode x (encode p)) p

 decEnc p = J (\x p -> Path (decode x (encode p)) p) q p where

 q : Path (decode a0 (encode refl)) refl

 q = transp (\i -> Path (decode a0 (encodeRefl (inot i))) refl) based