cubical type theory

[Thierry Coquand]

 We wrote a self-contained presentation of the formal system of cubical type 

theory.

Corresponding to this we have an updated version of our paper,

with a slightly improved algorithm for composition for

the glueing operation on types (section 6.2)

 Fabian Ruch has implemented in cubicaltt the proof of Corollary 10

which states that the type (Sigma X:U) Equiv X A   is contractible.

The proof is directly in normal form. It is then possible to deduce

from it the usual formulation of the univalence axiom (Corollary 11)

which we also implemented  in cubicaltt. This proof is not in normal

form, and its normal form is quite big (~12MB)...

This normal form was accepted by the type-checker but one can wonder

if there is a shorter normal form proof of Corollary 11.

 When using univalence for evaluating  closed terms of type Nat or Bool

we don’t need to compute this normal form, and such evaluation seems

reasonable (even for our naive implementation) for the small examples we

have tried so far.

 Thierry

PS:  Here are some further comments on this approach, 

after discussions at the meeting in Bonn.

The work of Nicola Gambino and Christian Sattler 

 http://arxiv.org/abs/1510.00669 shows how to adapt the notion of "uniform Kan filling

operation” to the setting of simplicial

sets and shows e.g. how to interpret constructively dependent products in this setting.

(However, It is not clear yet if univalence can be interpreted in this way

in a simplicial framework.)

 The following is a suggestive description of this uniformity condition

for the definition of Kan contractible sets. (A related description was considered

by André Joyal).  

We work in the topos of simplicial sets, and let \Omega

be its sub object classifier. Let partial(X) be the polynomial functor associated to 

true: 1 -> \Omega.

We have a canonical map   X -> partial(X): any total element can be seen as a partial

element.

 Definition: A simplicial set X is Kan and

contractible if, and only if, there is a retraction partial(X) -> X of the canonical

map X -> partial(X).

 Intuitively this means that X is Kan and contractible if

any partial element of X can be extended to a total element. 

 It follows from Theorem 5.7 in the paper of Nicola

and Christian that this definition is classically equivalent to the usual one.

 

 This corresponds to Section 5.1 in our paper.

In our setting, \Omega is replaced by a sub lattice (and we use this restriction

for interpreting univalence.)