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 = transpFill {\i -> B} (f.1 a) (inot 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


								sigmaPath : {A : Type} {B : A -> Type} {s1 : (x : A) * B x} {s2 : (x : A) * B x}

								         -> (p : Path s1.1 s2.1)

								         -> PathP (\i -> B (p i)) s1.2 s2.2

								         -> Path s1 s2

								sigmaPath p q i = (p i, q i)


								propExt : {A : Type} {B : Type}

								       -> isProp A -> isProp B

								       -> (A -> B)

								       -> (B -> A)

								       -> Equiv A B

								propExt {A} {B} propA propB f g = (f, contract) where

								  contract : (y : B) -> isContr (fiber f y)

								  contract y =

								    let arg : A

								        arg = g y

								     in ( (arg, propB y (f arg))

								        , \fib -> sigmaPath (propA _ _) (isProp_isSet {B} propB y (f fib.1) _ _))


								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)


								Bool_isSet : isHSet Bool

								Bool_isSet = pathToEq_isSet {Bool} (\{x} {y} -> p x y) where

								  p : (x : Bool) (y : Bool) -> Path x y -> Eq_s x y

								  p = \case

								    true -> \case

								      true -> \p -> refl_s

								      false -> \p -> absurd (trueNotFalse p)

								    false -> \case

								      false -> \p -> refl_s

								      true -> \p -> absurd (trueNotFalse (sym p))


								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)


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

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


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

								baseLoop_to_S1Map {X} p = \case

								  base -> p.1

								  loop i -> p.2 i


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

								S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, baseLoop_to_S1Map, ret, sec) where

								  to = S1Map_to_baseLoop

								  fro = baseLoop_to_S1Map


								  sec : {X : Type} -> (f : S1 -> X) -> Path (fro (to f)) f

								  sec {X} f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where

								    h : (x : S1) -> Path (fro (to f) x) (f x)

								    h = \case

								      base -> refl

								      loop i -> refl


								  ret : {X : Type} -> (x : (a : X) * Path a a) -> Path (to (fro x)) x

								  ret x = refl


								-- 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 _, 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 _ (encode p)) p

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

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

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


								S1_elim : (P : S1 -> Type)

								       -> (pb : P base)

								       -> PathP (\i -> P (loop i)) pb pb

								       -> (x : S1) -> P x

								S1_elim P pb pq = \case

								  base -> pb

								  loop i -> pq i


								PathP_is_Path : (P : I -> Type) (p : P i0) (q : P i1) -> Path (PathP P p q) (Path {P i1} (transp (\i -> P i) p) q)

								PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill {\j -> P j} p i) q


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

								Constant f = (y : B) * (x : A) -> Path y (f x)


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

								Weakly f = (x : A) (y : A) -> Path (f x) (f y)


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

								Conditionally f = (f' : Sq A -> B) * Path f (\x -> f' (inc x))


								Constant_weakly : {A : Type} {B : Type} (f : A -> B) -> Constant f -> Weakly f

								Constant_weakly f p x y = trans (sym (p.2 x)) (p.2 y)


								Constant_conditionally : {A : Type} {B : Type} -> (f : A -> B) -> Constant f -> Conditionally f

								Constant_conditionally {A} {B} f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where

								  c_const : Path f (\y -> p.1)

								  c_const i x = p.2 x (inot i)


								  const_c : (y : B) -> Conditionally {A} (\x -> y)

								  const_c y = (\x -> y, refl)


								S1_connected : (f : S1 -> Bool) -> Constant f

								S1_connected f = (f'.1, p) where

								  f' : (x : Bool) * Path x x

								  f' = S1Map_to_baseLoop f


								  p : (y : S1) -> Path f'.1 (f y)

								  p = S1_elim P refl loopc where

								    P : S1 -> Type

								    P = \y -> Path f'.1 (f y)


								    rr = refl {Bool} {f base}


								    loopc : PathP (\i -> P (loop i)) rr rr

								    loopc = transp (\i -> PathP_is_Path (\i -> P (loop i)) rr rr (inot i))

								              (Bool_isSet _ _ rr (transp (\i -> P (loop i)) rr))


								isProp_isEquiv : {A : Type} {B : Type} {f : A -> B} -> isProp (isEquiv f)

								isProp_isEquiv {f} p q i y =

								  let

								    p2 = (p y).2

								    q2 = (q y).2

								  in

								    ( p2 (q y).1 i

								    , \w j -> hcomp (\k [ (i = i0) -> p2 w j

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

								                        , (j = i0) -> p2 (q2 w (inot k)) i

								                        , (j = i1) -> w ])

								                    (inS (p2 w (ior i j)))

								    )


								isProp_EqvSq : {P : Type} (x : Equiv P (Sq P)) (y : Equiv P (Sq P)) -> Path x y

								isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (\i -> isEquiv (x1_is_y1 i)) x.2) y.2) where

								  x1_is_y1 : Path x.1 y.1

								  x1_is_y1 i e = sq (x.1 e) (y.1 e) i


								equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B}

								          -> Path e.1 e'.1

								          -> Path e e'

								equivLemma {A} {B} {e} {e'} p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2)


								isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)

								isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where

								  proj : Sq P -> P

								  proj = Sq_rec prop (\x -> x)


								  sqProp : isProp (Sq P)

								  sqProp x y i = sq x y i


								Sq_equiv_to_isProp : {P : Type} -> Equiv P (Sq P) -> isProp P

								Sq_equiv_to_isProp eqv = transp (\i -> isProp (univalence eqv (inot i))) (\x y i -> sq x y i)


								exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P))

								exercise_3_21 {P} = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp


								uaBeta : {A : Type} {B : Type} (e : Equiv A B) -> Path (idToEquiv (univalence e)).1 e.1

								uaBeta {A} {B} e i a = univalenceBeta e i a


								uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B})

								uaret eqv = equivLemma (uaBeta eqv)


								f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B

								f1 {A} p = (p.1, univalence p.2)


								f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B

								f2 {A} p = (p.1, idToEquiv p.2)


								uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a

								uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2)


								retContr : {A : Type} {B : Type}

								        -> (f : A -> B) -> (g : B -> A)

								        -> (h : retract f g)

								        -> isContr B -> isContr A

								retContr {A} {B} f g h v = (g b, p) where

								  b = v.1


								  p : (x : A) -> Path (g b) x

								  p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i)))