Zulip Chat Archive

Stream: Type theory

Topic: Model structure on simplicial sets


view this post on Zulip Bhavik Mehta (May 13 2020 at 19:16):

Moving here before we get told off

view this post on Zulip Reid Barton (May 13 2020 at 19:19):

Oops, maybe I noticed this too late :upside_down:

view this post on Zulip 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."

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Jalex Stark (May 13 2020 at 19:21):

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

view this post on Zulip Jalex Stark (May 13 2020 at 19:22):

what's "the Elephant"?

view this post on Zulip Mario Carneiro (May 13 2020 at 19:22):

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

view this post on Zulip Bhavik Mehta (May 13 2020 at 19:23):

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

view this post on Zulip Jalex Stark (May 13 2020 at 19:23):

thanks

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (May 13 2020 at 19:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 13 2020 at 19:36):

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

view this post on Zulip Bhavik Mehta (May 13 2020 at 19:36):

Do these tactics already exist? :o

view this post on Zulip Mario Carneiro (May 13 2020 at 19:36):

no

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 13 2020 at 19:42):

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

view this post on Zulip Jalex Stark (May 13 2020 at 19:42):

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

view this post on Zulip Mario Carneiro (May 13 2020 at 19:43):

Yes. Search for "dirichlet's theorem"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Reid Barton (May 16 2020 at 08:58):

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

view this post on Zulip 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