Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
To: Steve Awodey <awodey@cmu.edu>
Cc: "Michael Shulman" <shulman@sandiego.edu>,
	"Anders Mörtberg" <andersmortberg@gmail.com>,
	"Homotopy Type Theory" <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] A unifying cartesian cubical type theory
Date: Sun, 17 Feb 2019 10:43:30 +0100	[thread overview]
Message-ID: <20190217094330.GB3415@mathematik.tu-darmstadt.de> (raw)
In-Reply-To: <CA9EE7F9-87BD-4511-B6D4-891B946CD1B3@cmu.edu>

> 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.


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.

  reply	other threads:[~2019-02-17  9:43 UTC|newest]

Thread overview: 18+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-02-14 19:04 Anders Mortberg
2019-02-14 20:06 ` Andrew Pitts
2019-02-15 15:38   ` Anders Mörtberg
2019-02-15  8:16 ` Bas Spitters
2019-02-15 16:32   ` Anders Mörtberg
2019-02-16  0:01     ` Michael Shulman
2019-02-16  0:14       ` Steve Awodey
2019-02-16 12:30         ` streicher
2019-02-16 19:51           ` Thomas Streicher
2019-02-16 22:27             ` Steve Awodey
2019-02-17  9:43               ` Thomas Streicher [this message]
2019-02-17 14:14                 ` Licata, Dan
2019-02-16 21:58           ` Richard Williamson
2019-02-17  9:15             ` Thomas Streicher
2019-02-17 13:49               ` Richard Williamson
2019-02-18 14:05 ` [HoTT] " Andrew Swan
2019-02-18 15:31   ` Anders Mörtberg
2019-06-16 16:04     ` Anders Mörtberg

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20190217094330.GB3415@mathematik.tu-darmstadt.de \
    --to=streicher@mathematik.tu-darmstadt.de \
    --cc=andersmortberg@gmail.com \
    --cc=awodey@cmu.edu \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=shulman@sandiego.edu \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).