Philip Stassen: An Analysis of Curiens Explicit Syntax for Dependent Type Theory
Time: Mon 2020-03-30 11.00 - 12.00
Location: Zoom, Meeting ID: 678 046 973
Participating: Philip Stassen
Supervisor: Peter Lumsdaine, Guillaume Brunerie
Categorical models of dependent type theories have been extensively studied over the years. A difficulty that arises is the coherence between syntactical and semantical substitution: The on-the-nose equalities of the syntax collide with the up-to-isomorphism equalities of categories. We say a model is ''strict'' if this mismatch is resolved and that it is ''weak'' if the mismatch persists.
We present two dependent type theories, one of which has an additional term constructor, the explicit coercion. Pierre-Louis Curien has proven that locally cartesian closed categories provide strict models for the latter syntax without having to strictify the pullback – thereby resolving the mismatch by destrictifying the syntax instead. The type theory with explicit coercions can thus be used as intermediate step towards weak models for normal dependent type theories.
We construct a lift from the normal type theory into the type theory that has explicit coercions. This function can then be used to prove coherence theorems and by that could serve as a tool to construct weak models for dependent type theories.