-- 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.
ap : {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)
ap f p i = f (p i)

-- These satisfy definitional equalities, like apComp and apId, which are
-- propositional in vanilla MLTT.
apComp : {A : Type} {B : Type} {C : Type}
           {f : A -> B} {g : B -> C} {x : A} {y : A}
           (p : Path x y)
        -> Path (ap g (ap f p)) (ap (\x -> g (f x)) p)
apComp p = refl

apId : {A : Type} {x : A} {y : A}
         (p : Path x y)
     -> Path (ap (id {A}) p) p
apId p = refl

-- Just like rearranging parentheses gives us ap, 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)

subst : {A : Type} (P : A -> Type) {x : A} {y : A} -> Path x y -> P x -> P y
subst P p x = transp (\i -> P (p i)) 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) -> u (iand i j) itIs1
             , (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

-- 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} -> Equiv A A
idEquiv {A} = (\x -> x, \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
--
ua : {A : Type} {B : Type} -> Equiv A B -> Path A B
ua {A} {B} equiv i =
  Glue B (\[ (i = i0) -> (A, equiv),
             (i = i1) -> (B, idEquiv) ]) 

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)

isEquivTransport : (A : I -> Type) -> isEquiv (transp A)
isEquivTransport A = (lineToEquiv A).2

-- 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 -> ua 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.

uaBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> ua f i)) f.1
uaBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i)

-- The terms ua + uaBeta suffice to prove the "full"
-- ua 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

JRefl : {A : Type} {x : A}
        (P : (y : A) -> Path x y -> Type)
        (d : P x (\i -> x))
     -> Path (J {A} {x} P d {x} (\i -> x)) d
JRefl P d i = transpFill {\i -> P x (\j -> x)} d (inot i)

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 = ua (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 ua
---------------------------
--
-- The classic example of ua 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 = ua (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 ua (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.
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

sucEquiv : Equiv Int Int
sucEquiv = IsoToEquiv (sucZ, (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 = ua 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 (goAround (pos n)) (\i -> loop i)
    backwards : Nat -> Path base base
    backwards = \case
      zero -> \i -> loop (inot i)
      succ n -> trans (goAround (neg n)) (\i -> loop (inot i))

windingGoAround : (n : Int) -> Path (winding (goAround n)) n
windingGoAround =
  \case
    pos n -> posCase n
    neg n -> negCase n
  where
    posCase : (n : Nat) -> Path (winding (goAround (pos n))) (pos n)
    posCase = \case
      zero -> refl
      succ n -> ap sucZ (posCase n)
    negCase : (n : Nat) -> Path (winding (goAround (neg n))) (neg n)
    negCase = \case
      zero -> refl
      succ n -> ap predZ (negCase n)

decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
decodeSquare = \case
    pos n -> posCase n
    neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
  where
    posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
    posCase = \case
      zero -> \i j -> loop (ior i (inot j))
      succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) 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} = ua (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 -> ap inl (sym (unitEta x))
    inr x -> ap 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 = ua (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

isProp_isContr : {A : Type} -> isProp (isContr A)
isProp_isContr {A} z0 z1 j =
  ( z0.2 z1.1 j
  , \x i -> hcomp {A} (\k [ (i = i0) -> z0.2 z1.1 j
                          , (i = i1) -> z0.2 x (ior j k)
                          , (j = i0) -> z0.2 x (iand i k)
                          , (j = i1) -> z1.2 x i ])
                      (inS (z0.2 (z1.2 x i) j))
  )

isContr_isProp : {A : Type} -> isContr A -> isProp A
isContr_isProp x a b i = hcomp (\k [ (i = i0) -> x.2 a k, (i = i1) -> x.2 b k ]) (inS x.1)

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 = ua (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 {S1} 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 = ua (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 {S2} base2 (iand (inot l) i)
                                       , (k = i0) -> merid base2 (iand (inot l) i)
                                       , (k = i1) -> merid {S2} 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) -> p.2 (u itIs1) 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 (ua 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

uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (ua {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, ua 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)

isContrRetract : {A : Type} {B : Type}
              -> (f : A -> B) -> (g : B -> A)
              -> (h : retract f g)
              -> isContr B -> isContr A
isContrRetract {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)))

curry : {A : Type} {B : A -> Type} {C : (x : A) -> B x -> Type}
     -> Path ((x : A) (y : B x) -> C x y) ((p : (x : A) * B x) -> C p.1 p.2)
curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where
  to : ((x : A) (y : B x) -> C x y) -> (p : (x : A) * B x) -> C p.1 p.2
  to f p = f p.1 p.2

  from : ((p : (x : A) * B x) -> C p.1 p.2) -> (x : A) (y : B x) -> C x y
  from f x y = f (x, y)

ContractibleIfInhabited : {A : Type} -> Path (A -> isContr A) (isProp A)
ContractibleIfInhabited {A} = IsoToId (to, from, toFrom, fromTo) where
  to : (A -> isContr A) -> isProp A
  to cont x y = trans (sym (p.2 x)) (p.2 y) where
    p = cont x

  from : isProp A -> A -> isContr A
  from prop x = (x, prop x)

  toFrom : (y : isProp A) -> Path (to (from y)) y
  toFrom y = isProp_isProp {A} (to (from y)) y

  fromTo : (y : A -> isContr A) -> Path (from (to y)) y
  fromTo y i a = isProp_isContr {A} (from (to y) a) (y a) i

data cone (A : Type) : Type where
  point  : cone A
  base   : A -> cone A
  side i : (x : A) -> cone A [ (i = i0) -> point, (i = i1) -> base x ]

ConeA_contr : {A : Type} -> isContr (cone A)
ConeA_contr {A} = (point, contr) where
  contr : (y : cone A) -> Path point y
  contr = \case
    point  -> refl
    base x -> \i -> side x i
    side x i -> \j -> side x (iand i j)

contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B)
contrSinglEquiv {B} = (center, contract) where
  center : (A : Type) * Equiv A B
  center = (B, idEquiv)

  contract : (p : (A : Type) * Equiv A B) -> Path center p
  contract w i =
    let
      sys : Partial (ior (inot i) i) ((A : Type) * Equiv A B)
      sys = \ [ (i = i0) -> center, (i = i1) -> w ]

      GlueB = Glue B sys

      unglueB : GlueB -> B
      unglueB x = unglue {B} (ior (inot i) i) {sys} x 

      unglueEquiv : isEquiv {GlueB} {B} unglueB
      unglueEquiv b =
        let
          ctr : fiber unglueB b
          ctr = ( glue {B} {ior (inot i) i} {sys} (\[ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.1 ])
                    (primComp (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
                , fill (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))

          contr : (v : fiber unglueB b) -> Path ctr v
          contr v j = ( glue {B} {ior (inot i) i} {sys}
                          (\[ (i = i0) -> v.2 j, (i = i1) -> ((w.2.2 b).2 v j).1 ])
                          (inS (comp (\i -> B)
                                  (\k [ (i = i0) -> v.2 (iand j k)
                                      , (i = i1) -> ((w.2.2 b).2 v j).2 k
                                      , (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
                                      , (j = i1) -> v.2 k
                                      ])
                                  (inS b)))
                      , fill (\j -> B) (\k [ (i = i0) -> v.2 (iand j k)
                                           , (i = i1) -> ((w.2.2 b).2 v j).2 k
                                           , (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
                                           , (j = i1) -> v.2 k
                                           ])
                                       (inS b)
                      )
        in (ctr, contr)
    in (GlueB, unglueB, unglueEquiv)

uaIdEquiv : {A : Type} -> Path (ua idEquiv) (\i -> A)
uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv))

EquivJ : (P : (X : Type) (Y : Type) -> Equiv X Y -> Type)
      -> ((X : Type) -> P X X idEquiv)
      -> {X : Type} {Y : Type} (E : Equiv X Y)
      -> P X Y E
EquivJ P p {X} {Y} E =
  subst {(X : Type) * Equiv X Y}
        (\x -> P x.1 Y x.2)
        (\i -> isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) i)
        (p Y)

pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) idEquiv

univalence : {A : Type} {B : Type} -> Equiv (Path A B) (Equiv A B)
univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where
  pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) idEquiv
  pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) idEquiv

  ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p
  ua_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where
    lemma : Path (ua (pathToEquiv (\i -> A))) (\i -> A)
    lemma = transp (\i -> Path (ua (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv

  pathToEquiv_ua : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (ua p)) p
  pathToEquiv_ua {A} {B} p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where
    lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv
    lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl

total : {A : Type} {P : A -> Type} {Q : A -> Type}
     -> ((x : A) -> P x -> Q x)
     -> ((x : A) * P x) -> ((x : A) * Q x)
total f p = (p.1, f p.1 p.2)

total_fibers : {A : Type} {P : A -> Type} {Q : A -> Type}
            -> {xv : (a : A) * Q a}
            -> (f : (el : A) -> P el -> Q el)
            -> Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where
  to : {xv : (a : A) * Q a} -> fiber (total f) xv -> fiber (f xv.1) xv.2
  to peq = J {(a : A) * Q a} {_} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2)

  fro : {xv : (a : A) * Q a} -> fiber (f xv.1) xv.2 -> fiber (total f) xv
  fro peq = ((xv.1, peq.1), \i -> (_, peq.2 i))

  toFro : {xv : (a : A) * Q a} -> (y : fiber (f xv.1) xv.2) -> Path (to (fro y)) y
  toFro {xv} peq =
    J {Q xv.1} {f xv.1 p}
      (\xv1 eq1 -> Path (to {(xv.1, xv1)} (fro (p, sym eq1))) (p, sym eq1))
      (JRefl {(a : A) * Q a} {(xv.1, f xv.1 peq.1)}
        (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))
      (sym eq)
    where p : P xv.1
          p = peq.1

          eq : Path {Q xv.1} xv.2 (f xv.1 p)
          eq = peq.2

  froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y
  froTo {xv} apeq =
    J {(a : A) * Q a} {total f (a, p)}
      (\xv1 eq1 -> Path (fro {_} (to {_} ((a, p), sym eq1))) ((a, p), sym eq1))
      (ap fro (JRefl {(a : A) * Q a} {(a, _)}
                (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)))
      (sym eq)
    where a : A
          a = apeq.1.1

          p : P a
          p = apeq.1.2

          eq : Path xv (total f (a, p))
          eq = apeq.2

fiberEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
          -> (f : (el : A) -> P el -> Q el)
          -> isEquiv (total f)
          -> (x : A) -> isEquiv (f x)
fiberEquiv f iseqv x y = isContrRetract {fiber (f x) y} {fiber (total f) (x, y)} eqv.2.1 eqv.1 eqv.2.2.1 (iseqv (x, y)) where
  eqv : Iso (fiber (total f) (x, y)) (fiber (f x) y)
  eqv = total_fibers f

totalEquiv : {A : Type} {P : A -> Type} {Q : A -> Type}
          -> (f : (el : A) -> P el -> Q el)
          -> ((x : A) -> isEquiv (f x))
          -> isEquiv (total f)
totalEquiv f iseqv xv = isContrRetract {fiber (total f) xv} {fiber (f xv.1) xv.2} eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where
  eqv : Iso (fiber (total f) xv) (fiber (f xv.1) xv.2)
  eqv = total_fibers f

contrIsEquiv : {A : Type} {B : Type} -> isContr A -> isContr B
            -> (f : A -> B) -> isEquiv f
contrIsEquiv cA cB f y = ((cA.1, isContr_isProp cB _ _), \v -> sigmaPath (isContr_isProp cA _ _) (isProp_isSet (isContr_isProp cB) _ _ _ v.2))

theorem722 : {A : Type} {R : A -> A -> Type}
          -> ((x : A) (y : A) -> isProp (R x y))
          -> ({x : A} -> R x x)
          -> (f : (x : A) (y : A) -> R x y -> Path x y)
          -> {x : A} {y : A} -> isEquiv {R x y} {Path x y} (f x y)
theorem722 {A} {R} prop rho toId {x} {y} = fiberEquiv {A} {R x} {Path x} (toId x) (totalEquiv x) y where
  rContr : (x : A) -> isContr ((y : A) * R x y)
  rContr x = ((x, rho {x}), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2))

  totalEquiv : (x : A) -> isEquiv (total {A} {R x} {Path x} (toId x))
  totalEquiv x = contrIsEquiv (rContr x) singContr (total {A} {R x} {Path x} (toId x))