less prototype, less bad code implementation of CCHM type theory
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

#### 887 lines 30 KiB Raw Blame History

 `-- 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 : Type) -> A -> A` `the A x = x` ``` ``` `-- The eliminator for the interval says that if you have x : A i0 and y : A i1,` `-- and x ≡ y, then you can get a proof A i for every element of the interval.` `iElim : {A : I -> Type} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i` `iElim p i = p i` ``` ``` `-- This corresponds to the elimination principle for the HIT` `-- data I : Pretype where` `-- i0 i1 : I` `-- seg : i0 ≡ i1` ``` ``` `-- The singleton subtype of A at x is the type of elements of y which` `-- are equal to x.` `Singl : (A : Type) -> A -> Type` `Singl A x = (y : A) * Path x y` ``` ``` `-- Contractible types are those for which there exists an element to which` `-- all others are equal.` `isContr : Type -> Type` `isContr A = (x : A) * ((y : A) -> Path x y)` ``` ``` `-- Using the connection \i j -> y.2 (iand i j), we can prove that` `-- singletons are contracible. Together with transport later on,` `-- we get the J elimination principle of paths.` `singContr : {A : Type} {a : A} -> isContr (Singl A a)` `singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))` ``` ``` `-- Some more operations on paths. By rearranging parentheses we get a` `-- proof that the images of equal elements are themselves equal.` `cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)` `cong f p i = f (p i)` ``` ``` `-- These satisfy definitional equalities, like congComp and congId, which are` `-- propositional in vanilla MLTT.` `congComp : {A : Type} {B : Type} {C : Type}` ` {f : A -> B} {g : B -> C} {x : A} {y : A}` ` (p : Path x y)` ` -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)` `congComp p = refl` ``` ``` `congId : {A : Type} {x : A} {y : A}` ` (p : Path x y)` ` -> Path (cong (id {A}) p) p` `congId p = refl` ``` ``` `-- Just like rearranging parentheses gives us cong, swapping the value` `-- and interval binders gives us function extensionality.` `funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}` ` (h : (x : A) -> Path (f x) (g x))` ` -> Path f g` `funext h i x = h x i` ``` ``` `-- The proposition associated with an element of the interval` `-------------------------------------------------------------` ``` ``` `-- 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` `{-# PRIMITIVE IsOne #-}` ``` ``` `-- The value itIs1 witnesses the fact that i1 = i1.` `itIs1 : IsOne i1` ``` ``` `{-# PRIMITIVE itIs1 #-}` ``` ``` `-- 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.` ``` ``` `comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1` `{-# PRIMITIVE comp #-}` ``` ``` `-- In particular, when φ is a disjunction of the form` `-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a` `-- "tube", an open square with no floor or roof:` `--` `-- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,` `-- we draw:` `--` `-- x q i1` `-- | |` `-- \j -> x | | \j -> q j` `-- | |` `-- x q i0` `--` `-- The composition operation says that, as long as we can provide a` `-- "floor" connecting x -- q i0, as a total element of A which, on` `-- phi, extends u i0, then we get the "roof" connecting x and q i1` `-- for free.` `--` `-- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the` `-- "floor", and composition gets us the dotted line:` `-- ` `-- x..........z` `-- | |` `-- x | | q j` `-- | |` `-- x----------y` `-- p i` ``` ``` `trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z` `trans {A} {x} p q i =` ` comp (\i -> A)` ` {ior i (inot i)}` ` (\j [ (i = i0) -> x, (i = i1) -> q j ])` ` (inS (p i))` ``` ``` `-- In particular when the formula φ = i0 we get the "opposite face" to a` `-- single point, which corresponds to transport.` ``` ``` `transp : (A : I -> Type) (x : A i0) -> A i1` `transp A x = comp A {i0} (\i [ ]) (inS x)` ``` ``` `-- Since we have the iand operator, we can also derive the *filler* of a cube,` `-- which connects the given face and the output of composition.` ``` ``` `fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i` `fill A {phi} u a0 i =` ` comp (\j -> A (iand i j))` ` {ior phi (inot i)}` ` (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])` ` (inS (outS a0))` ``` ``` `hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> I -> A` `hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i` ``` ``` `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` ``` ``` `-- 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)` ``` ``` `-- 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` ``` ``` `-- 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 (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 {A} {B} 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 {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 (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 #-}` ``` ``` `-- 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)` ``` ``` `-- 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}) ]) ` ``` ``` ``` ``` `-- 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` ``` ``` `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` ``` ``` ``` ``` `-- 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 (f x0) y) (p1 : Path (f x1) y)` ` -> 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 i)))` ``` ``` ` rem1 : Path x1 (g y)` ` rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 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 i) ` ` ])` ` (inS (g (p0 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 i) ])` ` (inS (g (p1 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 j) k` ` , (i = i1) -> s (p1 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 j)` ``` ``` ` fCenter : (y : B) -> fiber f y` ` fCenter y = (g y, 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` ``` ``` `-- 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.` ``` ``` `bottom : Type` `bottom = {A : Type} -> A` ``` ``` `elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b` `elimBottom P x = x` ``` ``` `-- 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 {A} = transp (\i -> if (Bool -> Bool) A (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)` `--` `isHSet : Type -> Type` `isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q` ``` ``` `-- 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 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)` ``` ``` `-- The type of integers can be defined as A + B, where "pos n" means +n` `-- and "neg n" means -(n + 1).` ``` ``` `data Int : Type where` ` pos : Nat -> Int` ` neg : Nat -> Int` ``` ``` `-- On this representation we can define the successor and predecessor` `-- functions by (nested) induction.` ``` ``` `sucZ : Int -> Int` `sucZ = \case` ` pos n -> pos (succ n)` ` neg n ->` ` let suc_neg : Nat -> Int` ` suc_neg = \case` ` zero -> pos zero` ` succ n -> neg n` ` in suc_neg n` ``` ``` `predZ : Int -> Int` `predZ = \case` ` pos n ->` ` let pred_pos : Nat -> Int` ` pred_pos = \case` ` zero -> neg zero` ` succ n -> pos n` ` in pred_pos n` ` neg n -> neg (succ n)` ``` ``` `-- And prove that the successor function is an isomorphism, and thus, an` `-- equivalence.` ``` ``` `sucEquiv : isIso sucZ` `sucEquiv = ` ` let` ` sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x` ` sucPredZ = \case` ` pos n ->` ` let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)` ` k = \case` ` zero -> refl` ` succ n -> refl` ` in k n` ` neg n -> refl` ` predSucZ : (x : Int) -> Path (predZ (sucZ x)) x` ` predSucZ = \case` ` pos n -> refl` ` neg n ->` ` let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)` ` k = \case` ` zero -> refl` ` succ n -> refl` ` in k n` ` in (predZ, sucPredZ, predSucZ)` ``` ``` `-- Univalence gives us a path between integers such that transp intPath` `-- x = suc x, transp (sym intPath) x = pred x` ``` ``` `intPath : Path Int Int` `intPath = univalence (IsoToEquiv (sucZ, sucEquiv))` ``` ``` `-- Higher inductive types` `-------------------------` `--` `-- While inductive types let us generate discrete spaces like the` `-- naturals or integers, they do not support defining higher-dimensional` `-- structures given by spaces with points and paths.` ``` ``` `-- A very simple higher inductive type is the interval, given by` ``` ``` `data Interval : Type where` ` ii0 : Interval` ` ii1 : Interval` ` seg i : Interval [ (i = i0) -> ii0, (i = i1) -> ii1 ]` ``` ``` `-- This expresses that we have two points ii0 and ii1 and a path (\i ->` `-- seg i) with endpoints ii0 and ii1.` ``` ``` `-- With this type we can reproduce the proof of Lemma 6.3.2 from the` `-- HoTT book:` ``` ``` `iFunext : {A : Type} {B : A -> Type} (f : (x : A) -> B x) (g : (x : A) -> B x) -> ((x : A) -> Path (f x) (g x)) -> Path f g` `iFunext f g p i = h' (seg i) where` ` h : (x : A) -> Interval -> B x` ` h x = \case` ` ii0 -> f x` ` ii1 -> g x` ` seg i -> p x i` ``` ``` ` h' : Interval -> (x : A) -> B x` ` h' i x = h x i ` ``` ``` `-- Of course, Cubical Type Theory also has an interval (pre)type, but` `-- that, unlike the Interval here, is not Kan: it has no composition` `-- structure.` ``` ``` `-- Another simple higher-inductive type is the circle, with a point and` `-- a non-trivial loop, (\i -> loop i).` ``` ``` `data S1 : Type where` ` base : S1` ` loop i : S1 [ (i = i1) -> base, (i = i0) -> base ]` ``` ``` `-- By writing a function from the circle to the universe of types Type,` `-- we can calculate winding numbers along the circle.` ``` ``` `helix : S1 -> Type` `helix = \case` ` base -> Int` ` loop i -> intPath i` ``` ``` `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` ``` ``` `-- 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` ``` ``` `poSusp : Type -> Type` `poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt)` ``` ``` `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` ``` ``` `unitEta : (x : Unit) -> Path x tt` `unitEta = \case tt -> refl` ``` ``` `poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x` `poSusp_to_Susp_to_poSusp {A} = \case` ` inl x -> cong inl (sym (unitEta x))` ` inr x -> cong inr (sym (unitEta x))` ` push x i -> refl` ``` ``` `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}))`