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.
 
 
 

896 lines
30 KiB

-- 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
-- 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 (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
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 (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}))