A type system where univalence is provable. Here is a selfcontained presentation of the rules of this type system.
We show that singular cubical sets have the uniform Kan filling condition
We present the rules of a cubical type theory, corresponding to an implementation in Haskell, where we can transform isomorphisms to equality, and where we can represent higher-inductive types.
Using the framework of the note below, we show how to interpret higher inductive types in the cubical set model (second version; first version December 15 2014). This is the first occurence of the decomposition of composition in homogeneous composition and transport, which could be salvaged in the cubical set model when it was discovered that regularity does not hold. Like the extension from the first model to having diagonal, this discovery was motivated by the implementation of this model in Hasekll. Later Simon Huber discovered a nice simplification which was incorporated in the second version of the presentation of cubical type theory. (In each case, the respective contributions are listed at the end of the paper on cubical type theory.)
We add connections to the notion of cubes used in the cubical set model. We should now have better definitional equalities. This is the 3rd version. First version 8 September 2014. Before that, there was an attempt using only diagonals. first version April 9 2014 and second version September 1 2014
A small remark on two different formulations of the elimination rule for the identity type
In the framework of nominal sets with 01-substitution, we show that a contractible type has the property that any boundary of a box can be filled. This is used to give a computational way to transform an equivalence into a path between types (December 2013). There was an ad-hoc way suggested to improve this to a justification of univalence with yet another operation which was not really necessary. This operation of transforming an equivalence into a path was generalized to the "glueing" or "equivalence extension property" operation. (Surprisingly, it turned out that this equivalence extension property was also what was used by Vladimir Voevodsky for justifying univalence.)
A constructive version of Voevodsky's model of Kan simplicial sets (jww Marc Bezem and Simon Huber). Here are some slides (Bern, September 2013) presenting this model. This nominal interpretation of cubical sets was found by thinking about R. Williamson's course notes on combinatorial homotopy theory, asking the question: how can cubical sets be a model of type theory with the axiom of univalence?
A simple case of the setoid model gives a computational interpretation of Church's description axiom. This can be contrasted with a previous attempt which does not provide a convenient notion of definitional equality.
A variation on the setoid model where we get some definitional equality holding in the model. Hopefully this should be enough to interpret weak type theory. This generalizes to get an interpretation in intensional type theory of a weak form of the groupoid model.
The first published version of dependent type theory allows only a weak notion of conversion. The original version uses a system of combinators. We give an alternative formulation. It may be argued, and has been argued by Martin-Lof at some point, that this version represents a better notion of definitional equality.
One main obstacle for interpreting constructively the Kan simplicial set model of type theory is that degeneracy of simplices may not be decidable. This is explained in this paper. It is possible to transform computationally any weak equivalence between two such sets into a path between then (axiom of univalence).
A talk which should give a rather concrete explanation of the model of types as Kan simplicial sets. This gives a model of type theory with equality satisfying the extensionality axiom. However Kan condition is replaced by a more complex property and it is not clear if univalence holds in this model.
Talk in Stockholm (December 2011). Towards a constructive version of Kan simplicial sets, limited to the case of dimension < 2.
A revised version of the Bologna talk
A talk given for the 24th AILA meeting, Bologna, February 2011. I try to present V. Voevodsky Univalent Foundation. A new aspect may be a purely axiomatic presentation of equality. (All the proofs have been formally verified in Agda by Nils Anders Danielsson.)