## Stream: Type theory

### Topic: Model structure on simplicial sets

#### Bhavik Mehta (May 13 2020 at 19:16):

Moving here before we get told off

#### Reid Barton (May 13 2020 at 19:19):

Oops, maybe I noticed this too late :upside_down:

#### Jalex Stark (May 13 2020 at 19:20):

Trying to unpack this
"This becomes more than a philosophical issue with the relevance of this model category-structure in homotopy type theory, where internalization into the type theory requires constructive methods for interpreting proofs as programs."

#### Jalex Stark (May 13 2020 at 19:21):

is "interpreting proofs as programs" something that you need in order to build any theory at all?

#### Jalex Stark (May 13 2020 at 19:21):

can one use the "hacky classical model" to prove the first five or twenty pages of an HoTT book?

#### Bhavik Mehta (May 13 2020 at 19:21):

My best guess is something like: when you have a category with enough structure, you can interpret logic inside of it, and oftentimes phrasing proofs in the internal logic turns out to be easier (there's lots of examples in Section D of the Elephant, such as D.1.3.13 and D.1.3.14) - this is the internalization part at least.

#### Jalex Stark (May 13 2020 at 19:21):

I guess I say "an HoTT book" but maybe this is the canonical one?

#### Jalex Stark (May 13 2020 at 19:22):

what's "the Elephant"?

#### Mario Carneiro (May 13 2020 at 19:22):

https://www.amazon.com/Sketches-Elephant-Theory-Compendium-Oxford/dp/019852496X

#### Bhavik Mehta (May 13 2020 at 19:23):

https://ncatlab.org/nlab/show/Elephant

thanks

#### Bhavik Mehta (May 13 2020 at 19:24):

Speculating even further now, but this idea carries further when you define more internal notions, eg an internal ring or an internal category, and then if you proved your theorems constructively, their proofs should carry over exactly into the internal logic

#### Mario Carneiro (May 13 2020 at 19:25):

I think that this process of "internalized logic in a category" is the whole story of how HoTT became a foundation: first it was a category structure, then it grew so many structures that you can do logic in it, then people decided to use it as the metalogic and forget about the ambient logic (whatever it was)

#### Reid Barton (May 13 2020 at 19:25):

Reid Barton said:

Actually now I can't find anything about the other structure (with all monomorphisms as cofibrations); hopefully I didn't hallucinate it.

I didn't hallucinate it but I did somewhat misremember it, and it seems to not (yet) be known to be part of a model category. So, at the moment it seems that there is actually one clearly correct way to define the classical model structure with the correct constructive interpretation.

#### Mario Carneiro (May 13 2020 at 19:26):

and that's what the HoTT book uses - it is all logic "internal" to HoTT, which can also be interpreted as constructions inside a model of HoTT in a metalogic (classical or otherwise)

#### Reid Barton (May 13 2020 at 19:26):

I actually don't know exactly why people are interested in building models constructively, but they definitely are, see the pdf I linked in the other thread. I always assumed it was something to do with a computational interpretation.

#### Bhavik Mehta (May 13 2020 at 19:27):

Reid Barton said:

I actually don't know exactly why people are interested in building models constructively, but they definitely are, see the pdf I linked in the other thread. I always assumed it was something to do with a computational interpretation.

My guess is exactly this internalisation idea

#### Reid Barton (May 13 2020 at 19:27):

(And I still don't really understand what that means.)

#### Mario Carneiro (May 13 2020 at 19:27):

In particular, in order to interpret HoTT as having something to do with homotopy theory, you need to be working in a metalogic that can formalize homotopy theory and a suitable category of homotopy types that is a model of HoTT

#### Bhavik Mehta (May 13 2020 at 19:34):

A more practical example of internalisation: in Prop 1.1 of https://arxiv.org/pdf/1908.08488.pdf, she constructs an object of the category using (a suitable fragment of) the language of set theory, and discusses how the proof is just the usual set theory proof

#### Reid Barton (May 13 2020 at 19:35):

This internal interpretation is used for example in https://arxiv.org/abs/1912.10407 but I don't think it's the main reason why people are interested

#### Bhavik Mehta (May 13 2020 at 19:35):

More simply, if I have a ring object in a (sufficiently structured) category then any constructive proof about rings still holds in the category

#### Mario Carneiro (May 13 2020 at 19:35):

We have a mechanism for doing this, and that is using tactics for reflection, or tactics to conduct internal proofs

#### Reid Barton (May 13 2020 at 19:36):

The sentence in question ends with "interpreting proofs as programs"

#### Bhavik Mehta (May 13 2020 at 19:36):

Do these tactics already exist? :o

no

#### Bhavik Mehta (May 13 2020 at 19:37):

Yeah I was just about to continue and say that I don't see how internalisation relates to interpreting proofs as programs

#### Mario Carneiro (May 13 2020 at 19:37):

I think the most powerful form of this would be a proof translator that takes proofs in e.g. cubicaltt and reflects them into a model of cubical type theory in lean

#### Mario Carneiro (May 13 2020 at 19:37):

that way you get all the automation from a proof assistant that is actually designed for writing proofs in the internal language

#### Reid Barton (May 13 2020 at 19:38):

So there is apparently some model structure on cubical sets that satisfies univalence and can be used to model HoTT, and it's constructive, and I think this is supposed to be related to why cubical type theory satisfies canonicity or whatever.

#### Mario Carneiro (May 13 2020 at 19:38):

I guess you could say that my work in MM0 -> lean translation is an instance of such a thing

#### Reid Barton (May 13 2020 at 19:38):

But there is a whole lot of machinery between the syntax of HoTT and a model category that I don't understand, so it's unclear to me what the exact relationship is.

#### Mario Carneiro (May 13 2020 at 19:39):

since it takes proofs in ZFC in metamath and translates them to proofs about the type Set in lean

#### Jalex Stark (May 13 2020 at 19:41):

Mario Carneiro said:

I guess you could say that my work in MM0 -> lean translation is an instance of such a thing

#### Mario Carneiro (May 13 2020 at 19:42):

It is one section in the MM0 paper, it was also discussed here on zulip a while ago

#### Jalex Stark (May 13 2020 at 19:42):

https://arxiv.org/pdf/1910.10703.pdf
this one?

#### Jalex Stark (May 13 2020 at 19:42):

thanks, sorry. I tried finding a list of all your papers but wasn't able to

#### Mario Carneiro (May 13 2020 at 19:43):

Yes. Search for "dirichlet's theorem"

#### Mario Carneiro (May 13 2020 at 19:44):

Here's the original zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336

#### Bhavik Mehta (May 14 2020 at 11:25):

For the record I'm gonna weaken my position on wanting the hott model to be constructive - though I'd still aesthetically like it I wouldn't have any objection to starting off with going full classical

#### Valery Isaev (May 16 2020 at 01:41):

Reid Barton said:

Reid Barton said:

Actually now I can't find anything about the other structure (with all monomorphisms as cofibrations); hopefully I didn't hallucinate it.

I didn't hallucinate it but I did somewhat misremember it, and it seems to not (yet) be known to be part of a model category. So, at the moment it seems that there is actually one clearly correct way to define the classical model structure with the correct constructive interpretation.

So, what's this supposed model structure? Is it written anywhere?

#### Reid Barton (May 16 2020 at 08:57):

All I know about it is https://hott.github.io/HoTT-2019//conf-slides/van-den-Berg.pdf

#### Reid Barton (May 16 2020 at 08:58):

Cofibrations are the decidable monomorphisms, not the Reedy decidable monomorphisms.

#### Valery Isaev (May 16 2020 at 12:17):

Interesting. I always thought that the fact that not all simplicial sets are cofibrant is a major drawback of the constructive approach.

Last updated: May 18 2021 at 10:14 UTC