Maths - Cubical Type Theory

There is a problem with modeling spaces in this way in the consistency of higher order equalities.

To maintain consistency we need to model in a a less direct way by using the map out of an interval.

\func coe (P : I -> \Type)
          (a : P left)
          (i : I) : P i \elim i
  | left => a

On the page here we looked at proofs in a more traditional Martin-Löf theory.

When implemented (modeled) in Idris it is shown as an equality which we understand as a proposition.

(plus x Z) = x

Refl

Path nat (add zero n) n

<i> zero

total plusZeroRightNeutral : (x : Nat) -> (plus x Z) = x
plusZeroRightNeutral Z     = Refl
plusZeroRightNeutral (S n) = rewrite (plusZeroRightNeutral n) 
                                                     in Refl

add_zero : (n : nat) -> Path nat (add zero n) n = split
  zero  -> <i> zero
  suc n -> <i> suc (add_zero n @ i)

Where:

• PathP is a heterogeneous path type and is a builtin keyword.
• Path is a homogeneous path type and is defined here as a map from the interval <i> to 'a'.

So, instead of modeling '=' directly, it is instead modeled indirectly as 'Path'.

-- Identity types

Path (A : U) (a0 a1 : A) : U = PathP (<i> A) a0 a1

refl (A : U) (a : A) : Path A a a =<i> a

Here (from this site) the second type of equality is constructed . Transporting true along this equality gives false and false gives true.

isoToEquiv : type of A, type of B, A->B,B->A,y->path B,x->path A

notK is a proof that not not b = b

notEquiv : equiv bool bool =
  (not,isoToEquiv bool bool not not notK notK)

-- Construct an equality in the universe using Glue
notEq : Path U bool bool =
   Glue bool [ (i = 0) -> (bool,notEquiv)
                , (i = 1) -> (bool,idEquiv bool) ]

-- The fiber/preimage of a map:
fiber (A B : U) (f : A -> B) (y : B) : U =
  (x : A) * Path B y (f x)

-- A map is an equivalence if its fibers are contractible
isEquiv (A B : U) (f : A -> B) : U =
  (y : B) -> isContr (fiber A B f y)

Nat n
n -> (n = n+0)

When using cubical type theory we can specify variables in the formal interval:

If 'C' is the context, containing the variables, then C^op is the formal interval and a path is a presheaf C^op->Set.

-- Identity types

Path (A : U) (a0 a1 : A) : U = PathP (<i> A) a0 a1

refl (A : U) (a : A) : Path A a a =<i> a

used for variables i...

with grammar

r,s ::= 0 | 1 | i | 1-r | r/\s | r\/s

where:

• 0 is least element 0:(1->)
• 1 is greatest element 1:(1->)
• r,s are variables
• r/\s is meet representing min /\:(->->)
• r\/s is join representing max \/:(->->)
• 1-r is an involution (its own inverse)
  • where:
    • 1-0=1
    • 1-1=0
    • 1-(r\/s) = (1-r)/\(1-s)
    • 1-(r/\s) = (1-r)\/(1-s)
  • (1-r):(->)

Path_Ax y behaves like a function out of the interval p:-> A

where:

• p 0 = x
• p 1 = y

Althoughis not a proper type so we can't have a function into it for example.

If we have a type B and a partial type A that is equivalent to B where it is defined then we can glue them together to form a new type.

from Orton, R. I. (2019). Cubical Models of Homotopy Type Theory - An Internal Approach (Doctoral thesis). https://doi.org/10.17863/CAM.36690

Here is an example of a binary type with two elements '0' and '1'.

This type can be 'equal' to inself in two ways:

• 0=0 and 1=1 or,
• 0=1 and 1=0

Glue  :{L L'} (A : Set L) {φ : I}
     -> Partial φ (Σ[TSet L'] TA) -> Set L'

glue :{ L L'} {A : Set L} {φ : I}
	   {Te : Partial φ ( Σ[TSet L'] 
	            TA)}
     -> PartialP φ T -> A -> Glue A Te

unglue :{ L L'} {A : Set L} (φ : I) 
	  {Te : Partial φ (Σ[TSet L' ]
	            TA)}
       -> Glue A Te -> A

Where:

• Partial - allows Agda to define partially specified n-dimensional cubes.
• Setω - allows Agda to make sure everything has a 'type' in the presence of universe polymorphism.

Partial :{L} -> I -> Set L -> Setω

For traditional equalities and equivalences we have a relatively simple concept of transitivity to combine them.

So in the case illustrated here:

• A=B
• B=C

so we can deduce

• A=C

This could be extended to multiple equalities which might be illustrated by a diagram like this where the missing face of a polygon can be inferred.

This is related to a Horn clause discussed on page here.

However, when we move to homotopy type equalities things get more complicated, we need to make sure all possible paths between the endpoints are included.

See the discussion of composition of paths on page here.

We have already looks at the 'bool' example. Here is slightly more complicated so that we can think about composition.

So imagine a type which is a list containg the elements: 'x', 'y' and 'z'.

If we have another list with these elements, but in a different order, then this would be isomorphic (but not equal) to the original list.

Presheaf Example - Single Element Set

A very simple example would be where C^op is a single element set (terminal object in set).

Hom( C^op, Set) therefore contains set of single arrows, one for every element of the set.

Presheaf Example - Graph

Here C^op is a category with two objects E (for edge) and V (for vertex) also two arrows s (for source) and t (for target).

This allows us to build a structure on top of set where the diagram on the right commutes.

We can therefore build up complex graphs from individual vertices and edges.

Presheaf - Interval

Proposition

a=b

Path

I->A
may still use a=b

Proof of that proposition

Refl: a=a

Recap

So if we have 2 points 'n' and 'n+0' are they on a path/surface? This corresponds to the proposition 'n=n+0'. If we we using Boolean logic this proposition would be either true or false. In M-L type theory/constructive logic the proposition is either proven or its not, if its not then we can't say anything about it. Here the truth value is a free De Morgan algebra.

A cubical complex might be thought of as a family of types where the cells are put into are hierarchy of types according to their dimension.

These dimensions (and therefore types) are related by their boundary maps,

where:
F(f) : F(Y) -> F(X) is the function mapping each occurrence y of Y in F to the corresponding suboccurrence x (included in y through f) of X in F

• https://agda.readthedocs.io/en/v2.6.1/language/cubical.htmlx
• https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html

• https://github.com/mortberg/cubicaltt/blob/master/lectures/lecture2.ctt

• home
• tutorial
• code on github