|
-- 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
|
|
|
|
-- Furthermore, if either of i or j are one, then so is (i or j).
|
|
isOneL : {i : I} {j : I} -> IsOne i -> IsOne (ior i j)
|
|
isOneR : {i : I} {j : I} -> IsOne j -> IsOne (ior i j)
|
|
|
|
{-# PRIMITIVE itIs1 #-}
|
|
{-# PRIMITIVE isOneL #-}
|
|
{-# PRIMITIVE isOneR #-}
|
|
|
|
-- 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 (\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))
|
|
|
|
-- 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 f y)
|
|
|
|
-- By extracting this point, which must exist because the fiber is contractible,
|
|
-- we can get an inverse of f:
|
|
|
|
inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
|
|
inverse eqv y = (eqv y) .1 .1
|
|
|
|
-- We can prove that «inverse eqv» is a section of f:
|
|
|
|
section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
|
|
section f eqv i y = (eqv y) .1 .2 i
|
|
|
|
-- Proving that it's also a retraction is left as an exercise to the
|
|
-- reader. We can package together a function and a proof that it's an
|
|
-- equivalence to get a capital-E Equivalence.
|
|
|
|
Equiv : (A : Type) (B : Type) -> Type
|
|
Equiv A B = (f : A -> B) * isEquiv f
|
|
|
|
-- 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
|