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