Model structure on simplicial sets

Stream: Type theory

[Bhavik Mehta]

Moving here before we get told off

[Reid Barton]

Oops, maybe I noticed this too late :upside_down:

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Bhavik Mehta]

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]

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

[Jalex Stark]

what's "the Elephant"?

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Jalex Stark]

thanks

[Bhavik Mehta]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Reid Barton]

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

[Bhavik Mehta]

Do these tactics already exist? :o

[Mario Carneiro]

no

[Bhavik Mehta]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Jalex Stark]

Mario Carneiro said:

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

do you have a paper / library one should read to learn about this?

[Mario Carneiro]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

Yes. Search for "dirichlet's theorem"

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

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

[Valery Isaev]

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