Skip to main content
MathOverflow

Return to Question

replaced http://mathoverflow.net/ with https://mathoverflow.net/
Source Link
Community Bot
Community Bot
  • 1
  • 2
  • 3

While thinking about Jason Rute's questionJason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed the univalence phenomenon. However, it is not clear that HoTT is intended to describe this model as opposed to groupoid models or a broader class of models.

A related question is whether there is a notion of standard model for HoTT. That is, a notion comparable in role to ω-models for second-order arithmetic and transitive/well-founded models for set-theory.

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed the univalence phenomenon. However, it is not clear that HoTT is intended to describe this model as opposed to groupoid models or a broader class of models.

A related question is whether there is a notion of standard model for HoTT. That is, a notion comparable in role to ω-models for second-order arithmetic and transitive/well-founded models for set-theory.

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed the univalence phenomenon. However, it is not clear that HoTT is intended to describe this model as opposed to groupoid models or a broader class of models.

A related question is whether there is a notion of standard model for HoTT. That is, a notion comparable in role to ω-models for second-order arithmetic and transitive/well-founded models for set-theory.

Source Link
François G. Dorais
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Are simplicial sets the intended model of HoTT?

While thinking about Jason Rute's question, I wondered if there was an intended model for HoTT. The main candidate for the intended model are simplicial sets, where Vladimir Voevodsky first observed the univalence phenomenon. However, it is not clear that HoTT is intended to describe this model as opposed to groupoid models or a broader class of models.

A related question is whether there is a notion of standard model for HoTT. That is, a notion comparable in role to ω-models for second-order arithmetic and transitive/well-founded models for set-theory.