Re: [HoTT] A unifying cartesian cubical type theory

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

> I don???t want to minimize the importance of the work on cubical type theory 
> ??? which I believe is very great ??? but it has focussed on building models of type theory 
> directly, often within other type theories, rather than on building Quillen model categories. 
> To be sure, many ideas, and some terminology, from model category theory are used, 
> but without showing or even claiming that there is a Quillen model structure.

They didn't emphasize model structures but they are around and more
explicitly in Sattler's work. Admittedly, there are sometimes
distinctions which only make sense if the meta theory is constructive.
But if one ignores that then they are interpreting syntax in minimal
Cisinski model structures defined by open box filling conditions.
One does know that minimal and test model structure fall apart when
taking as site free finitely generated de Morgan algebras as shown by Sattler.
It is unknown when taking the "cartesian site" of finite lattices and
monotone maps between them (opposite to free finitely generated
distributive lattices and homomorphisms).
I agree that in the published papers on cubical TT the model category
aspect is not shown bluntly but Thierry is aware of it and it shows up
in Christian's work quite explicitly.

Moreover, I think it is not important to choose the minimal Cisinski
model structures as one can interpret Cubical TT also in the test
model structure on cubical sets. There are fewer fibrations since
there are more anodyne cofibrations but when interpreting syntax one
stays within this more restricted collection of fibrations.

The only problem with simplical sets is that finite powers of the
interval are not representable. That's overcome by choosing the cubical
site. But one may still restrict fibrations to those of the test model
structure and one gets the simplical set model when restricting the
fibration to simplicial sets.

Thomas

PS  Thierry insists on constructing models in constructive meta
theories like CZF with universes or extensional type theory with
universes. This has the benefit of obtaining conservation results but
is not necessary for the interpreted theories having computational meaning.
The theories have their computational meaning independently from the
models they are interpreted in.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.