Maths - Cubical Type Theory

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

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

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 occurance y of Y in F to the corresponding suboccurrence x (included in y through f) of X in F