From 4ad87302c140c86ee29a4236f03a52efdc2256f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Sat, 27 Feb 2021 23:18:09 -0300 Subject: [PATCH] Document glueing + univalence --- intro.tt | 161 ++++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 148 insertions(+), 13 deletions(-) diff --git a/intro.tt b/intro.tt index 233fd4c..af66f2c 100644 --- a/intro.tt +++ b/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 \ No newline at end of file +-- 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