Maths - Cubical Type Theory (CTT)

On the page here Martin-Löf type theories are introduced and here is a discussion of how it can be used in the Idris language.

The aim of this page is to combine these ideas with:

• Homotopy Type Theory (HoTT)
• Cubical Sets

This motivation is very hand-wavy, it is not intended to be rigorous, its just my attempt to get some intuition.

To prove weaker forms of equality such as isomorphism we usually have two functions between the objects and require some equations to be true. This is an external, category theory, type of approach which requires some functions/arrows to exist but doesn't say exactly what they are. What we want here is to internalise it and make it more constructive.

What happens when there are a sequence of edges following each other? (the target of the first is equal to the source of the second and so on). Can the edge in the intervalmatch the whole path?

Is this the same thing as requiring composition?

See the page about the graph category for more theory behind this.

In cubical type theory equalities are represented by a path, in a given space, between equal terms.

A path can be defined like a function out of the interval

p:-> A

However, when denoted like that, the endpoints are not visible outside the function (at compile time) so its better to internalise it (with the endpoints as parameters) so the endpoints are visible and denote it like this:

Path_Ax y

where:

• p 0 = x
• p 1 = y

Althoughis not strictly a type so we have to be careful how we work with it, we can't have a function into it for example.

A map out of an interval is not strictly a function, if it was a function it could be constructed with a lambda function like this:

p=λi.expression(i)

but it is still a binding of the variable 'i' so instead we write it like this:

p=<i>expression(i)

An interval spaceis a space with two points and a path between them.

The interval is like a type, we think of functions from it. Technically it is not exactly a type, for instance, we can't have functions into it.

For the reasons discussed on this page we instead work more indirectly in terms of a map out of the interval into Nat. This gives a more indirect notion of path denoted by Path in cubicaltt.

When we have a function like x->y we interpret this as y for all x.

So-> Nat gives a type for all values along the interval.

The n -> at the start shows we want a path that is true for all numbers.

So we interpret the whole thing as an equality between the interpretation of n and the interpretation of n+0.

If we want to prove n=n+0 for all n we want to prove,

• 0=0+0
• 1=1+0
• 2=2+0
• and so on

but since Nat is infinite we can never do it in this way.

However Nat is defined inductively so we can prove this using induction.

We can think of this hom functor Cube^op -> set as picking out all cases of a shape (in this case cubes) in set.

Presheaf Example - Graph

See this page.

Presheaf - Interval

A fibration allows us to 'lift' a line between two points to a line between two structures. This is called the homotopy lifting property (HLP).

In this diagram the blue lines show the mapping of points and the green line maps lines (like open set) in the opposite direction to the points.

A cofibration allows us to 'extend' a mapping from a subset to a mapping from the whole structure. This is called the homotopy extension property (HEP).

Again the blue lines show the mapping of points and the green line maps lines (like open set) in the opposite direction to the points.

We are given 3 categories 'C', 'D' and 'E' and 2 functors F:C->E and K:C->D.

The Kan extension tries to find some unique functors between D and E:

Here we want to use this concept in cubical type theory:

So, using the left Kan extension, C becomes the interval, D and E become types we want to compare.

We can extend this concept to higher dimensional intervals (for example a square). Provided only one face is missing the orther one can be filled in

See fill function on this site.

In order to program with these concepts we may need the ability to work with individual arrows (partial functions).

Extending one end extends the other.

Example from Arend Language

The function coe defines dependent eliminator for I, it says that in order to define f : \Pi (i : I) -> P i
for some P : I -> \Type it is enough to specify f left

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

We want to compose two paths:

• Path A x y
• Path A y z

These correspond to the bottom and right arrows on this diagram:

Their composition is the arrow on the top.

Meet

Here we have two variables i and j. We want to look at p at i/\j which is given by:

<i,j>p@(i/\j)

by substituting 0 and 1 into various combinations of i and j we can get expressions for the edges and points on the diagram:

Join

In this case we look at p at i\/j which is given by:

<i,j>p@(i\/j)

and again we substitute 0 and 1 into various combinations of i and j:

This path represents a proposition. To prove the proposition we need to construct the type. As this type is a function that is an implementation of the function.

p: Path Set a b is a proposition in set.

We can make a proposition of equality between any two elements.

<.> x:p is a constructor for this proposition, an implementation of the function out of the interval, so it is a proof of the proposition.

In set we can only construct Path Set a a , so this is like Refl for set

Instances of the product type are a tuple.

If we require (a,b)=(c,d)

then we need a=c and b=d.

(eliminator for product type).

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.

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) ]

-- contractible type
isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y)

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

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.

a,b:Nat

a=b

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

If we have two topological spaces X & Y with two continuous maps between them F & G then a homotopy is a continuous map between F & G.

In order to see how this is related to the map between the cup and torus I have drawn a map from a third shape (in this case another torus).

So as F continuously maps the G then the cup maps to the torus.

We can move the continuous map forward from the functions to the domain so the functions are homotopic if:

H: X × [0,1] -> Y

where:

• H(x,0) = F(x)
• H(x,1) = G(x)

We can think of this as 'filling in' the gap between F and G so that we can take any path through it.