amelia
/
cubical


								-- 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 -> Pretype) -> A i0 -> A i1 -> Type

								{-# PRIMITIVE PathP #-}


								-- By taking the first argument to be constant we get the equality type

								-- Path.


								Path : {A : Pretype} -> A -> A -> Type

								Path {A} = PathP (\i -> A)


								-- reflexivity is given by constant paths


								refl : {A : Pretype} {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 -> Pretype} {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 -> Pretype} {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))

								         (\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.