-- 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 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) 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 -> 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 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 = 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. 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 = univalence 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} = 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 -> 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 = 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 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 = 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 {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 = 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 {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) 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 uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B}) uaret eqv = equivLemma (univalenceBeta 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))) 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) ft2 : {A : Type} -> Path (T2 -> A) (S1 -> S1 -> A) ft2 {A} = transp (\i -> Path (T2 -> A) (curry {S1} {\x -> S1} {\x y -> A} (inot i))) p where p : Path (T2 -> A) ((S1 * S1) -> A) p i = TorusIsTwoCircles i -> A data coeq {A : Type} {B : Type} (f : B -> A) (g : B -> A) : Type where c : A -> coeq {A} {B} f g p i : (b : B) -> coeq {A} {B} f g [ (i = i0) -> c (f b), (i = i1) -> c (g b) ] coeq_S1 : Type coeq_S1 = coeq {Unit} {Unit} id id coeq_base : coeq_S1 coeq_base = c tt coeq_loop : Path coeq_base coeq_base coeq_loop i = p tt i coeq_S1_elim : (P : coeq_S1 -> Type) (base : P coeq_base) -> PathP (\i -> P (coeq_loop i)) base base -> (x : coeq_S1) -> P x coeq_S1_elim P base loop = \case c x -> baseCase x p x i -> loopCase x i where baseCase : (x : Unit) -> P (c x) baseCase = \case tt -> base loopCase : (x : Unit) -> PathP (\i -> P (p x i)) (baseCase x) (baseCase x) loopCase = \case tt -> loop 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, the B, idEquiv {B}) 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 (univalence (the A, idEquiv {A})) (\i -> A) uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, the A, idEquiv {A})) EquivJ : {X : Type} (P : (Y : Type) -> Equiv Y X -> Type) (d : P X (the X, idEquiv {X})) {Y : Type} (E : Equiv Y X) -> P Y E EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d where path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e) path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e) uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B) uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A}) pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A}) pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A}) univalence_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (univalence (pathToEquiv p)) p univalence_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (univalence {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where lemma : Path (univalence (pathToEquiv (\i -> A))) (\i -> A) lemma = transp (\i -> Path (univalence (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv pathToEquiv_univalence : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (univalence p)) p pathToEquiv_univalence {A} {B} p = EquivJ {B} (\A e -> Path (pathToEquiv (univalence e)) e) lemma p where lemma : Path (pathToEquiv (univalence (the B, idEquiv {B}))) (the B, idEquiv {B}) lemma = transp (\i -> Path (pathToEquiv (uaIdEquiv {B} (inot i))) (the B, idEquiv {B})) pathToEquiv_refl uaEquiv : {A : Type} {B : Type} -> isEquiv (pathToEquiv {A} {B}) uaEquiv {A} {B} = (IsoToEquiv (uaIso {A} {B})).2