Document glueing + univalence

intro.tt

@@ -299,33 +299,168 @@ transpFun p q f = refl
 -- 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 (f x) y
 
+-- 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 f y)
 
+-- By extracting this point, which must exist because the fiber is contractible,
+-- we can get an inverse of f:
+
+inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
+inverse eqv y = (eqv y) .1 .1
+
+-- We can prove that «inverse eqv» is a section of f:
+
+section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
+section f eqv i y = (eqv y) .1 .2 i
+
+-- 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 f
 
-primGlue : (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
+-- 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 (inot i), \j -> u.2 (ior (inot 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 #-}
-prim'Glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> (e o).1 (t o)) -> primGlue A T e
-{-# PRIMITIVE glue prim'Glue #-}
-primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> primGlue A {phi} T e -> A
+
+-- 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 #-}
+
+-- 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 #-}
 
+-- 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)
 
-idEquiv : {A : Type} -> isEquiv (id {A})
-idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))
-
+-- 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}) ]) 
+univalence {A} {B} equiv i =
+  Glue B (\[ (i = i0) -> (A, equiv),
+             (i = i1) -> (B, the B, idEquiv {B}) ]) 
 
-A, B : Type
-f : Equiv A B
-x : A
-line : I -> Type
-line i = univalence {A} {B} f i
+-- The fact that this diagram has 2 filled-in B sides explains the
+-- complication in the proof below.
+--
+-- In particular, the actual behaviour of transp (\i -> univalence f i)
+-- (x : A) is not just to apply f x to get a B (the left side), it also
+-- needs to:
+--
+--   * For the bottom side, compose along (\i -> B) (the bottom side)
+--   * For the right side, apply the inverse of the identity, which
+--     is just identity, to get *some* b : B
+-- 
+-- But that b : B might not agree with the sides of the composition
+-- operation in a more general case, so it composes along (\i -> B)
+-- *again*!
+--
+-- Thus the proof: a simple cubical argument suffices, since
+-- for any composition, its filler connects either endpoints. So
+-- we need to come up with a filler for the bottom and right faces.
+
+univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1
+univalenceBeta {A} {B} f i a =
+  let
+    -- The bottom left corner
+    botLeft : B
+    botLeft = transp (\i -> B) (f.1 a)
+
+    -- The "bottom face" filler connects the bottom-left corner, f.1 a,
+    -- and the bottom-right corner, which is the transport of f.1 a
+    -- along \i -> B.
+    botFace : Path (f.1 a) botLeft
+    botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i
+
+    -- The "right face" filler connects the bottom-right corner and the
+    -- upper-right corner, which is again a simple transport along
+    -- \i -> B.
+    rightFace : Path (transp (\i -> B) botLeft) botLeft
+    rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)
+
+    -- The goal is a path between the bottom-left and top-right corners,
+    -- which we can get by composing (in the path sense) the bottom and
+    -- right faces.
+    goal : Path (transp (\i -> B) botLeft) (f.1 a)
+    goal = trans rightFace (\i -> botFace (inot i))
+  in goal i
+
+-- The terms univalence + univalenceBeta suffice to prove the "full"
+-- univalence axiom of Voevodsky, as can be seen in the paper
+--
+--   Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom.
+--
+-- Available freely here: https://arxiv.org/abs/1712.04890v3