Zulip Chat Archive

Stream: Type theory

Topic: How to get HoTT people into Lean


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

a question from another stream: Is it necessary, when building a model of HoTT, to do it constructively?

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

My perspective is this: It's not necessary but it'd be nice. When dealing with this sort of foundational stuff it feels weird to me to use choice when it's not needed. Taking an example from set theory (because I'm sharper on set theory and category theory than HoTT), constructing an inner model of ZFC (eg ZF + V=L) from a model of ZF doesn't feel like an achievement if your metatheory assumed choice

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

I would argue that constructive mathematics isn't really appropriate for lean, in the sense that if you have a hard "yes, it must be constructive" answer to this, then you should use another proof assistant entirely like cubicaltt or something, because "constructive lean" isn't going to satisfy your constraints

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

I'm totally on board with "avoid choice until it becomes necessary" though

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

I'm also okay with "use choice but don't stop someone else reproving your things without choice"

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

I guess the concern is when it comes to a choice argument being more convenient

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

Oddly enough I think LEM is the main stumbling block, not that it matters much.

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

People from a set theory background think about these things differently than type theorists working in extensions of MLTT

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

Relatedly, for some topos stuff I'm playing with I only need 'unique choice' rather than full choice and again I don't much like the idea of using full choice to prove independence-like results related to choice

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

One of the first things you'd probably want is the classical model structure on simplicial sets, which doesn't need choice but in the absence of LEM "splits" into two different model structures.

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

That said I appreciate it would be unpleasant in lean to have some hierarchy of choice results, and I also appreciate the internal vs external arguments

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

So as soon as you write down a definition of this structure, you are committing to one or the other constructive interpretation (or neither, I guess)

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

If the metatheory, that is lean, is completely classical, then you don't have to mind the constructive interpretations

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

so it's not really a decision you can defer

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

Right, but then you score 0 on Bhavik's scale.

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

Reid Barton said:

So as soon as you write down a definition of this structure, you are committing to one or the other constructive interpretation (or neither, I guess)

Do you have anything I can read to learn more about this?

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

I'll try to dig up links (should be easy), or I can just tell you if you know a little about simplicial sets.

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

(I'm also not an expert on these particular constructive structures. Like, I don't know what "model category" actually means constructively.)

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

https://ncatlab.org/nlab/show/constructive+model+structure+on+simplicial+sets describes one of the structures

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

although probably https://arxiv.org/pdf/1907.05394.pdf is more readable than the nlab page about it

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

So it sounds like a person who had the goal "convince HoTT people to play with Lean" should non-constructively build a model of HoTT, and package it in such a way that it is clear what API a new model needs to satisfy, so that an incoming HoTT person could redo it constructively if they like

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

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

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

I also have a concern related to the idea which I think is expressed here: "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." but I don't know enough HoTT to argue either side

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

are there any people that both have this goal and know enough about HoTT?

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

can someone unpack that quote for me?

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

(I guess the reason I care about this at all is because I have the impression that some of the HoTT folks are very sharp and persuasive)

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

(it's from Reid's nlab link, by the way)

view this post on Zulip Jannis Limperg (May 13 2020 at 19:42):

The primary reason HoTT people aren't interested in Lean is not the classical vs constructive issue. HoTT is perfectly compatible with classical axioms; afair, even parts of the HoTT book use classical logic. (Some of the HoTT people are pretty hardcore constructivists though.) Besides, it would be possible, with some effort, to ensure that Lean's classical axioms are not used in any HoTT-based development.

Instead, the primary reason is that Lean's type theory implies axiom K (uniqueness of identity proofs), which contradicts univalence. This cannot be turned off or worked around, so you can't do axiomatic HoTT in Lean (and besides, with HoTT-based proof assistants like Cubical Agda now available, axiomatic HoTT doesn't look too hot anyway). Of course, you can still deeply embed HoTT into Lean and prove things about it, but it is not clear to me that this would be significantly easier than with any other proof assistant.

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

what do you mean by "deeply embed"?

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

is this morally equivalent to "build a model of HoTT"?

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

I think it's the embedding we're talking about - the idea is to do such an embedding (constructively or otherwise) and then get the HoTT people to work in/on it

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

I also don't see any reason that it would be easier to build a model of HoTT in Lean rather than another theorem prover, except insofar as you can ask questions on this server as you do it

view this post on Zulip Jannis Limperg (May 13 2020 at 19:45):

Deep embedding = "define the terms, typing judgements etc. of (some variant of) HoTT as inductive data types".

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

@Jannis Limperg , do you think that once that work is done, it would make sense to start "doing HoTT in Lean"?

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

in the same sense that many of us (who are content with Lean's dependent type theory foundations) already "do math in Lean"?

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

It would be impractical without a lot of automation.

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

To perform all the work that Lean normally does for you, like type checking, elaboration, etc. Ideally, one would somehow repurpose Lean itself for this but that's not something that just happens automatically.

view this post on Zulip Jannis Limperg (May 13 2020 at 19:51):

Jalex Stark said:

Jannis Limperg , do you think that once that work is done, it would make sense to start "doing HoTT in Lean"?

No, this would be extremely inconvenient. If you wanted to define the "HoTT natural numbers", you'd have to write HoTT terms (inhabitants of your term type, i.e. syntax trees) for all relevant definitions, then write proofs that these syntax trees are well-typed, then write proofs that they satisfy any definitional equalities you care about, etc. This could in principle be automated, but at that point you're implementing something like Cubical Agda within Lean.

Compare this with the situation in Coq or non-cubical Agda: You postulate the univalence axiom and otherwise use the proof assistant as usual.

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

ah interesting

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

so i guess the question at hand is "is it easier to write a HoTT theorem-prover from scratch or to implement one inside of Lean"

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

For example flypitch contains a deep embedding of first-order logic and its proof theory and the axioms of ZFC, but I don't think they ever actually write down proofs as terms in this way

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

Definitely from scratch

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

and the answer to that question right now is probably "from scratch"?

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

that's why it's been done so many times

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

Not least because it has already been done for you

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

But then you don't get a relative consistency proof, for example.

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

but what this doesn't give you is any of the meta properties like soundness or consistency or interpretation as theorems about homotopy theory

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

My question here is what exactly do HoTT people want to do when they "do HoTT"? Are they proving things inside the theory or proving things about the theory? In the latter case it's not clear to me why we care about the embedding being inconvenient (but I suspect the former is more likely)

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

When I look at HoTT papers, it's all external reasoning

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

(deleted)

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

the only people who do internal HoTT are people who actually work on the proof assistants

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

well, both; but the intended use of HoTT is to prove theorems in it, otherwise why are you interested in the metatheory?

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

I mean there's proofs of stuff like π4(S3)=Z/2\pi_4(S^3) = \mathbb{Z}/2 and stuff like that. Or Floris's Serre spectral sequence.

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

so how fragmented should the online formal theorem-proving community be? (like in equilibrium?)
proposed state of the world:
there's an ATP similar to lean, together with a userbase that doesn't care about foundations,
and for each popular foundational system whose type theory is incompatible with "native lean", there is another ATP with an associated community

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

I can't parse that last sentence

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

if you were responding to me, is that better?

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

Well, this seems like two questions: one about the tools, another about the communities around those tools.

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

I don't wish lean world domination at equilibrium

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

you can't have tools without communities to maintain them

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

do you wish "exists X, X world domination"?

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

But we can change these answers independently.

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

(I think i wish that, which is why i wrote lean* originally)

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

For example, we could decide that maybe there should just be a single "itp.zulipchat.com" while still having Lean, Coq, Agda etc.

view this post on Zulip Jalex Stark (May 13 2020 at 20:00):

ah you mean a community can write new ITPs and abandon old ones

view this post on Zulip Mario Carneiro (May 13 2020 at 20:00):

not really... more like there should be a cabal of mutually interpretable theorem provers with joint world domination

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

Or vice versa.

view this post on Zulip Jalex Stark (May 13 2020 at 20:00):

okay

view this post on Zulip Mario Carneiro (May 13 2020 at 20:00):

which isn't too far from current reality

view this post on Zulip Mario Carneiro (May 13 2020 at 20:01):

(except for the mutually interpretable part)

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

It's hard to write the single greatest possible theorem prover to rule them all, but easy (or at least differently hard) to bring people together into one community.

view this post on Zulip Johan Commelin (May 13 2020 at 20:01):

Mario Carneiro said:

which isn't too far from current reality

Well... and that part about world domination

view this post on Zulip Mario Carneiro (May 13 2020 at 20:02):

details

view this post on Zulip Jalex Stark (May 13 2020 at 20:02):

my view of mutual interpretability is that there's one ITP (maybe i'll call it MM0*?) which every serious new ATP wants to show bi-interpretability with

view this post on Zulip Jalex Stark (May 13 2020 at 20:02):

because you want only O(n) bi-interpretations instead of O(n^2)

view this post on Zulip Mario Carneiro (May 13 2020 at 20:03):

there are foundational issues with actual bi-interpretability, but you can get interpretability up to adding axioms in the target

view this post on Zulip Jalex Stark (May 13 2020 at 20:03):

(though in practice people will keep writing bi-interpretations between other pairs, and you'll end up with O(n log n) many bi-interpretations)

view this post on Zulip Mario Carneiro (May 13 2020 at 20:03):

that's fine

view this post on Zulip Jalex Stark (May 13 2020 at 20:04):

what is interpretability up to extra axioms?

view this post on Zulip Mario Carneiro (May 13 2020 at 20:04):

It might still be O(n) if the graph is a tree but not a star graph

view this post on Zulip Jalex Stark (May 13 2020 at 20:04):

does it allow for "automated translations"?

view this post on Zulip Jalex Stark (May 13 2020 at 20:04):

right, my point is just that it's not going to be a tree

view this post on Zulip Mario Carneiro (May 13 2020 at 20:05):

I can translate MM into HOL but MM supports ZFC and HOL is weaker than ZFC

view this post on Zulip Jalex Stark (May 13 2020 at 20:05):

because people like having fun, and if there's a unique root people will be sad about that

view this post on Zulip Jalex Stark (May 13 2020 at 20:05):

okay, does that mean the other direction wouldn't require extra axioms?

view this post on Zulip Mario Carneiro (May 13 2020 at 20:05):

A spanning tree has no designated root

view this post on Zulip Mario Carneiro (May 13 2020 at 20:06):

there might be non-tree parts if a composite translation can be done more efficiently directly

view this post on Zulip Mario Carneiro (May 13 2020 at 20:06):

Jalex Stark said:

okay, does that mean the other direction wouldn't require extra axioms?

In theory yes, in practice that depends on the quality of translation

view this post on Zulip Mario Carneiro (May 13 2020 at 20:07):

For example in the MM -> lean translation the raw translation gives you thousands of new axioms in lean

view this post on Zulip Mario Carneiro (May 13 2020 at 20:07):

and I had to go through and prove each of them as theorems

view this post on Zulip Jalex Stark (May 13 2020 at 20:07):

Mario Carneiro said:

A spanning tree has no designated root

right, thanks. the interpretation tree means that you get to trust all of the theorem provers if you trust any of their implementations
and if you don't trust any of them, you can write a new one and just link it into the tree

view this post on Zulip Mario Carneiro (May 13 2020 at 20:07):

(most are trivial because they are actually definitions)

view this post on Zulip Jalex Stark (May 13 2020 at 20:08):

okay so we already know constructions that do translation and they generate a bunch of extra goals

view this post on Zulip Jalex Stark (May 13 2020 at 20:09):

so a "higher quality translation" is just one that has automation for closing those goals

view this post on Zulip Mario Carneiro (May 13 2020 at 20:09):

In a sense that's where the actual mathematical work is

view this post on Zulip Jalex Stark (May 13 2020 at 20:09):

in particular, if Lean automation is very good, that makes interpreting things in Lean easier

view this post on Zulip Mario Carneiro (May 13 2020 at 20:09):

it generally can't be automated

view this post on Zulip Jalex Stark (May 13 2020 at 20:10):

the "not-very good translation" reduces the translation problem to doing math in the target theorem prover?

view this post on Zulip Mario Carneiro (May 13 2020 at 20:10):

for example if I prove a library of theorems about rings I can apply them to the type int but it leaves behind some proof obligations, namely to show that int is a ring

view this post on Zulip Jalex Stark (May 13 2020 at 20:11):

seems like the sort of proof obligation we're already good at automating?

view this post on Zulip Jalex Stark (May 13 2020 at 20:11):

by apply_instance?

view this post on Zulip Mario Carneiro (May 13 2020 at 20:11):

maybe I did some really complicated theorem about rings in a "ring theorem prover" that takes the axioms of rings for granted and proves some really complicated statement

view this post on Zulip Mario Carneiro (May 13 2020 at 20:12):

and now I can translate this proof to lean, where "ring" is relativized to a predicate on types rather than being a built in notion

view this post on Zulip Jalex Stark (May 13 2020 at 20:12):

and then you just have to prove once that the ring predicate on types is satisfied by any type with a ring instance?

view this post on Zulip Mario Carneiro (May 13 2020 at 20:12):

right

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

that seems like the kind of thing that software engineers do for a living

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

"here are two very similar APIs, plug them into each other"

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

For HoTT that means constructing simplicial sets and showing that they form a model of HoTT, and having a general translation that takes proofs from theorem prover X and produces a proof in lean in any model of HoTT

view this post on Zulip Mario Carneiro (May 13 2020 at 20:14):

sure, it's not a new idea by any stretch, nor is it an insurmountable task

view this post on Zulip Mario Carneiro (May 13 2020 at 20:15):

but if I was to do something like this for HoTT today there would be a big gap in the target (lean) because there is no definition of "model of HoTT" nor any construction satisfying that definition

view this post on Zulip Jalex Stark (May 13 2020 at 20:15):

okay, I thought we disagreed on whether this was automatable and I think we learned that I was just using a nonstandard definition of automation

view this post on Zulip Mario Carneiro (May 13 2020 at 20:16):

the part that can be automated is not that hard, but there is more to the story that requires attention from actual mathematicians

view this post on Zulip Mario Carneiro (May 13 2020 at 20:18):

and this is what I hope to convince HoTT-minded mathematicians to do

view this post on Zulip Jalex Stark (May 13 2020 at 20:18):

and the part that needs mathematicians is exactly "build a model of hott in lean"?

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

I see @Egbert Rijke in the chat...

view this post on Zulip Egbert Rijke (May 13 2020 at 22:19):

Hi @Mario Carneiro It is already late in Europe, I'll read up on this thread tomorrow.

But to get HoTT people interested in Lean, it would be nice if it wouldn't be inconsistent to assume the univalence axiom in Lean. The lean developers have closed the door for us a couple of years ago, and we weren't welcome anymore.

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

@Egbert Rijke (I've said this above but the short version is) Is the univalence axiom required to define models of HoTT though? The sort of mathematics that is done in your papers doesn't actually need univalence at the metalevel, right?

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

No, certainly not

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

I'm interested in capturing a rather different aspect of HoTT than that traditionally represented in existing HoTT theorem provers

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

@Reid Barton Do you know what the current state of HoTT foundations in lean are? I think something to do with simplicial sets is in lean, as well as a bunch of category theory that is not necessarily directly related to HoTT. Do you know what the roadmap would look like?

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

I know a lot about what the homotopy theory/model category side of things would look like (and eventually I'll get around to this), but not much about what the type theory side would look like.

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

I think the homotopy/category side is the limiting factor right now AFAIK

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

I imagine the type theory side is pretty simple, just defining an axiomatic description of a category with operations needed by HoTT

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

As I sort of suggested at #Type theory > externalization, one could consider the type theory side for an extensional type theory first.

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

Do we have topoi yet?

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

You could start with a lot less than Lean's type theory of course.

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

Well, there's https://github.com/b-mehta/topos

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

If the README is up to date then "soon"

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

How far are we from a category supporting MLTT without universes?

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

that might just be a topos, I'm not up on the lingo

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:30):

The relevant API is currently atrocious and badly documented (at least, most of the parts I wrote are), but I should be able to interpret and, or, exists so far

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:30):

Actually the readme is a bit out of date

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:31):

I never defined a typeclass topos but I've been using finite limits and has_power_objects which is the same thing

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

where do dependent pis come from?

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:31):

Actually I've also got points 2 and 4, (and 5 in a branch)

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:32):

I'd need to check my understanding of dependent pi but I have local cartesian closure

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:33):

I have this: https://ncatlab.org/nlab/show/dependent+product#in_toposes

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:33):

I'm not sure if the 'preserve' properties underneath are easy to get right now but I haven't thought about it

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

I guess the main new widget in HoTT models is infinity cats

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:34):

To the best of my knowledge that's nowhere in lean

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

although you might still be able to use a regular cat as a model

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

does univalence imply that it is necessarily non-strict at all h-levels?

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

Well technically I think the terminal/contractible (infinity-)category qualifies as a model :upside_down:

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

the empty perfectoid space of HoTT

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

perfect

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

obviously that's the right way to interpret π(S1)=Z\pi(S^1)=\mathbb{Z}

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

Otherwise it should, yes

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

Oh, well hmm. If you don't have HITs and only one universe, then I'm not sure.

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

I think there are still some tricky bits in the 1-categorical / extensional MLTT case that haven't been mentioned yet

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

we're supposed to associate to each thing in the syntax some kind of thing in the model

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

to each context, we're supposed to associate an object

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

and I'm pretty sure that definitionally equal contexts are supposed to get equal objects of the topos

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

that sounds right

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

and this means that certain constructions have to be strictified in some ways that otherwise wouldn't be natural

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

I think the example is that substitution is modelled by a pullback

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

oh, I think I see the issue

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

and so you need to choose for each ΓΓ\Gamma' \to \Gamma and AΓA \to \Gamma a specific pullback AΓA' \to \Gamma'

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

do you have to take a quotient of the objects or something?

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:42):

Reid Barton said:

and so you need to choose for each ΓΓ\Gamma' \to \Gamma and AΓA \to \Gamma a specific pullback AΓA' \to \Gamma'

I'm probably missing something but isn't this exactly what has_pullbacks encodes?

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

such that if you pull back again over another ΓΓ\Gamma'' \to \Gamma' you get the same AΓA'' \to \Gamma whether you did it in one step or two

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

but it's not just any choice of pullbacks, it needs to commute with something

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

Right, it also has to commute with basically everything in sight

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:43):

Fair, my second question then is, do you need equal objects or equal subobjects?

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

Like if you have a type former sum A B and you model it by A⨿BA \amalg B, then the chosen pullbacks also have to commute with the chosen ⨿\amalg s

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

They aren't subobjects. I guess if you were just doing propositional logic, then you would be fine because you have only "ΓAprop\Gamma \vdash A\,\mathrm{prop}" and this is modelled by a subobject

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:44):

In the logic case formulae are interpreted as subobjects of the object which represents the "space" of their free-variables

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

Anyways, there's various type theory/category theory gadgets which solve these coherence issues but I haven't learned about them.

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

Forgive my naivete, but shouldn't it be the work of an hour or something to write down "here is a category with sums and products and pullbacks and this commutes with that and ...." and get everything that an MLTT category needs?

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

Usually one thinks of these as somehow "intermediate" between the MLTT syntax and the semantic object (like a topos)

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

Maybe, I don't know exactly what the list is. Probably it depends too on how much stuff is in your type theory.

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

true, but hopefully the work is easily adapted to variations on the type theory

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

so it would be reasonable to target something simple but representative to start, like MLTT

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:49):

Reid Barton said:

They aren't subobjects. I guess if you were just doing propositional logic, then you would be fine because you have only "ΓAprop\Gamma \vdash A\,\mathrm{prop}" and this is modelled by a subobject

I'm skimming D4 in the elephant and he seems to be saying that it's fine for higher order logic

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

But this isn't something they teach in school and I have no idea where the type theorists start

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

does the elephant cover dependent type theory?

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:51):

https://ncatlab.org/nlab/show/Elephant#d4_higherorder_logic I don't think so

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:52):

It does talk about MLTT though in D4.4

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

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory

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

the ncatlab page makes a big deal about extensional vs intensional MLTT. I guess in the extensional version you don't need "on the nose" commutation of type formers and substitution

view this post on Zulip Bhavik Mehta (May 13 2020 at 22:57):

https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#DependentTypeTheory and things linking from it seem to have a lot of discussion about the coherence issues

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

Extensional basically just means you are in the 1-categorical setting I think.

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

If you want to model things using objects of a category, you still have an issue with coherence: whether two objects produced in different ways that the syntax thinks are the same are actually equal.

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

If you have a universe, though, then you can model a type as a map (since in general terms are going to be represented as certain maps, and now a type is also a term) and that makes things easier because maps are just equal or not equal.

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

At least in the 1-categorical setting. In a higher categorical setting now you would have a new kind of coherence problem I think.

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

Mario Carneiro said:

does the elephant cover dependent type theory?

Sorry it does!

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

From what I'm reading here it does seem like I could interpret MLTT...

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

Reid Barton said:

and I'm pretty sure that definitionally equal contexts are supposed to get equal objects of the topos

Ah the disparity is here I think - PTJ seems to consider contexts which are permutations of one another as not defeq

view this post on Zulip Mario Carneiro (May 13 2020 at 23:17):

in MLTT you can't even permute contexts, so this isn't a problem

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

I mean two contexts which you can permute

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

I think

view this post on Zulip Mario Carneiro (May 13 2020 at 23:18):

but you can perform substitution and this has to commute with everything

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

This is probably incredibly basic but here's how it interprets substitution, in this language could someone describe the categorical property that we need?

view this post on Zulip Mario Carneiro (May 13 2020 at 23:21):

What does the substitution of a type look like in that setting?

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

for example sum (A[t/y]) (B[t/y]) = (sum A B)[t/y]

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

Right, there is no problem for terms but there is for types.

view this post on Zulip Mario Carneiro (May 13 2020 at 23:24):

What even are types in this type theory? Is it Gamma |- A type or Gamma |- A : U where U is some special object?

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

Mario Carneiro said:

What even are types in this type theory? Is it Gamma |- A type or Gamma |- A : U where U is some special object?

image.png I think this answers your question?

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

I don't have a good answer for the earlier one though, I'm not seeing anything about equality of types right now

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

Oh hang on you're substituting a term inside a type

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

I don't think I have satisfying answers for you I'm reading this stuff for the first time

view this post on Zulip Mario Carneiro (May 13 2020 at 23:31):

So what is the interpretation of the ΓAΣTyp\Gamma \vdash A \in \Sigma-Typ judgment in the category? In the earlier quote it mentions Γt:B\Gamma\vdash t:B getting interpreted as a morphism t:MΓMBt:M\Gamma\to MB, but this suggests that MBMB is an object independent of Γ\Gamma

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

no mbox :frown:

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

image.png

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

image.png this precedes Def 4.4.3

view this post on Zulip Mario Carneiro (May 13 2020 at 23:35):

Oh I see, MBMB is actually abuse of notation

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

Now that I think about it, I'm pretty sure there was a talk at the HoTT conference in August which formalized the construction of an interpretation for some theory in Agda

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

https://hott.github.io/HoTT-2019//conf-slides/Brunerie.pdf

view this post on Zulip Mario Carneiro (May 13 2020 at 23:58):

Looks like they do take a quotient of the objects (slide 15)

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

I like the last line of the conclusion

view this post on Zulip Reid Barton (May 14 2020 at 00:00):

Well there's a quotient of the objects in the term model, which is why mapping out of it requires sending defeq contexts to equal objects

view this post on Zulip Reid Barton (May 14 2020 at 00:01):

There's still a separate question of how, given a locally cartesian closed category, one would cook up one of these contextual categories that satisfies all the required equations

view this post on Zulip Mario Carneiro (May 14 2020 at 00:01):

and they also use the partiality monad for defining the interpretation recursion mutual on everything in sight

view this post on Zulip Reid Barton (May 14 2020 at 00:02):

also, they're basically using Lean without axioms but apparently actually using Lean would be too easy so they implemented that in Agda instead

view this post on Zulip Mario Carneiro (May 14 2020 at 00:03):

agda users do seem to like to build everything from scratch

view this post on Zulip Reid Barton (May 14 2020 at 00:03):

ok they don't have large elimination for eq I guess

view this post on Zulip Reid Barton (May 14 2020 at 00:04):

https://github.com/guillaumebrunerie/initiality/blob/reflection/contextualcat.agda

view this post on Zulip Mario Carneiro (May 14 2020 at 00:04):

oh, ft stands for father

view this post on Zulip Reid Barton (May 14 2020 at 00:05):

oh that makes more sense than "foot"

view this post on Zulip Mario Carneiro (May 14 2020 at 00:06):

does anyone want to try transcribing CCat in lean?

view this post on Zulip Reid Barton (May 14 2020 at 00:08):

no

view this post on Zulip Mario Carneiro (May 14 2020 at 00:09):

Looking at it I don't think there is anything problematic in there

view this post on Zulip Reid Barton (May 14 2020 at 00:09):

It's just ... really long

view this post on Zulip Mario Carneiro (May 14 2020 at 00:10):

although the arrows are all jumbled up in one type per "grade" rather than sorted by dom/cod like in lean's categories

view this post on Zulip Bhavik Mehta (May 14 2020 at 00:10):

at least a third of it just looks like category axioms

view this post on Zulip Mario Carneiro (May 14 2020 at 00:11):

It is like category axioms, but not quite because it's graded

view this post on Zulip Bhavik Mehta (May 14 2020 at 00:11):

ah

view this post on Zulip Mario Carneiro (May 14 2020 at 00:11):

you would have to define these axioms and then construct a standard category on top

view this post on Zulip Reid Barton (May 14 2020 at 00:21):

So I think if you start with the category of sets, which is locally cartesian closed

view this post on Zulip Reid Barton (May 14 2020 at 00:22):

then the associated contextual category has

  • as objects, for each nn, strings XnX1X0=X_n \to \cdots \to X_1 \to X_0 = *
  • as morphisms from XnX1X0=X_n \to \cdots \to X_1 \to X_0 = * to YmY1Y0=Y_m \to \cdots \to Y_1 \to Y_0 = *, just maps XnYmX_n \to Y_m

view this post on Zulip Reid Barton (May 14 2020 at 00:26):

star takes a map from XnX1X0=X_n \to \cdots \to X_1 \to X_0 = * to YmY1Y0=Y_m \to \cdots \to Y_1 \to Y_0 = * and an extension Ym+1YmY_{m+1} \to Y_m \to \cdots to an extension Xn+1XnX_{n+1} \to X_n \to \cdots which is equipped with a map to Ym+1YmY_{m+1} \to Y_m \to \cdots, which I'm assuming is supposed to be some choice of pullback

view this post on Zulip Reid Barton (May 14 2020 at 00:26):

and then there is

    star-comp : {m n k :} {g : Mor m k} {f : Mor n m} {Y : Ob m} {f₁ : ∂₁ f ≡ Y} {g₀ : ∂₀ g ≡ Y}
      {X : Ob (suc k)} {Z : Ob k} {p : ft X ≡ Z} {g₁ : ∂₁ g ≡ Z} 
      star (comp g f g₀ f₁) X p (comp₁ ∙ g₁) ≡ star f (star g X p g₁) (ft-star ∙ g₀) f₁

view this post on Zulip Reid Barton (May 14 2020 at 00:28):

and I think this expresses
Reid Barton said:

such that if you pull back again over another ΓΓ\Gamma'' \to \Gamma' you get the same AΓA'' \to \Gamma whether you did it in one step or two

view this post on Zulip Reid Barton (May 14 2020 at 00:29):

where:

  • X is AA
  • Z is Γ\Gamma
  • Y is Γ\Gamma'
  • the unnamed source of f is Γ\Gamma''

view this post on Zulip Reid Barton (May 14 2020 at 00:29):

So, in order to write down the contextual category which corresponds to Set you first need to solve this coherence problem.

view this post on Zulip Reid Barton (May 14 2020 at 00:32):

then you'll need to repeat this feat for all the type formers you're interested in, for example

    SumStrNat' : (g : MorC n m) (Δ : Ob n) (g₀ : ∂₀ g ≡ Δ) (Γ : Ob m)
      (A : Ob (suc m)) (A= : ft A ≡ Γ) (B : Ob (suc m)) (B= : ft B ≡ Γ) (g₁ : ∂₁ g ≡ Γ) 
      star g (SumStr Γ A A= B B=) SumStr= g₁ ≡
        SumStr Δ (star g A A= g₁) (ft-star ∙ g₀) (star g B B= g₁) (ft-star ∙ g₀)

view this post on Zulip Mario Carneiro (May 14 2020 at 00:33):

Is this what they called "naturality" in the slides?

view this post on Zulip Reid Barton (May 14 2020 at 00:34):

It seems to be, though I would not otherwise have guessed that meaning

view this post on Zulip Reid Barton (May 14 2020 at 00:37):

I'm guessing they chose this approach because their notion of a contextual category (with XYZ...) is literally a model of a certain essentially algebraic theory (which, ironically, I think means they could basically have automated large parts of their formalization with suitable tactics?)

view this post on Zulip Bhavik Mehta (May 14 2020 at 00:39):

It looks pretty similar to https://ncatlab.org/nlab/show/categorical+model+of+dependent+types#contextual_categories_or_csystems

view this post on Zulip Reid Barton (May 14 2020 at 00:43):

Anyways, I think the sheer length of that nlab page indicates that bridging the gap between MLTT and a locally cartesian closed category is not a simple problem

view this post on Zulip Mario Carneiro (May 14 2020 at 00:45):

is this stuff actually usable? I guess the application of such a construction would be something like proving that pi(S^1) = Z in HoTT implies that pi(S^1) = Z in sets, but the translation overhead seems pretty ridiculous

view this post on Zulip Mario Carneiro (May 14 2020 at 00:46):

like what are the "unit tests" for this interpretation?

view this post on Zulip Reid Barton (May 14 2020 at 00:48):

I was thinking it would be funny to just interpret a proof about types back into Type and see how bad it gets.

view this post on Zulip Reid Barton (May 14 2020 at 00:48):

Another thing which is not perhaps obvious from that page but I think is true is that a fairly large amount of the work to bridge the gap doesn't depend on whether the thing on the other side is a 1-topos or an infinity-topos.

view this post on Zulip Reid Barton (May 14 2020 at 00:50):

For example from an infinity-topos (or more precisely from some choice of model category which models it, together with some choice of solution to the strictification problems) you also get out a contextual category, not some "contextual infinity-category".

view this post on Zulip Mario Carneiro (May 14 2020 at 00:50):

The page suggests Hofmann, "Syntax and semantics of dependent types" as a general reference

view this post on Zulip Mario Carneiro (May 14 2020 at 00:52):

The definition of a contextual category in ncatlab is a strict category, while I think Brunerie's is not

view this post on Zulip Egbert Rijke (May 14 2020 at 09:48):

Mario Carneiro said:

Forgive my naivete, but shouldn't it be the work of an hour or something to write down "here is a category with sums and products and pullbacks and this commutes with that and ...." and get everything that an MLTT category needs?

The problem in defining models of HoTT is not so much to interpret Pi and Sigma. After you've gone through the coherence theorems, the real problem is to construct univalent universes that are closed under all the type theoretic operations, preferably including higher inductive types.

view this post on Zulip Egbert Rijke (May 14 2020 at 09:50):

This was a major advance by Mike Shulman. You can read about it here.

view this post on Zulip Mario Carneiro (May 14 2020 at 09:50):

right, but this is more of a mathematical problem. I'm thinking more about the CS-y, fiddly bits that go into formalizing all this

view this post on Zulip Mario Carneiro (May 14 2020 at 09:51):

I'm assuming that the mathematical problems have all been solved at this point

view this post on Zulip Mario Carneiro (May 14 2020 at 09:51):

at least, for the basics of "there exists a nontrivial model of HoTT"

view this post on Zulip Mario Carneiro (May 14 2020 at 09:55):

"We begin with some 2-categorical observations. A morphism f:XYf:X→Y in a 2-category KK is an internal fibration if each induced functor K(Z,X)K(Z,Y)K(Z,X)→K(Z,Y) is a Grothendieck fibration." This clearly isn't going to be intelligible to me

view this post on Zulip Egbert Rijke (May 14 2020 at 09:55):

To really have a theorem like that, you first have to define in Lean the syntax of HoTT. Do you have any theories in Lean, formulated syntactically?

view this post on Zulip Mario Carneiro (May 14 2020 at 09:55):

sure, we've done it before, not for MLTT and extensions though

view this post on Zulip Mario Carneiro (May 14 2020 at 09:56):

Floris and Jesse wrote the syntax of FOL and ZFC in lean and proved soundness and completeness for FOL

view this post on Zulip Reid Barton (May 14 2020 at 09:56):

A better starting point would be https://arxiv.org/abs/1211.2851

view this post on Zulip Egbert Rijke (May 14 2020 at 09:56):

Ok, then I assume that you have all you need

view this post on Zulip Johan Commelin (May 14 2020 at 09:57):

Sounds like a nice exercise for your students in that 2 week course (-;

view this post on Zulip Mario Carneiro (May 14 2020 at 09:57):

in the technical sense yes, but we need a type theorist who knows the terrain, and that's not me

view this post on Zulip Mario Carneiro (May 14 2020 at 09:57):

possibly reid or bhavik can fill that role

view this post on Zulip Mario Carneiro (May 14 2020 at 09:58):

Certainly you can, if you are willing

view this post on Zulip Mario Carneiro (May 14 2020 at 10:02):

Appendix B of https://arxiv.org/abs/1211.2851 looks promising

view this post on Zulip Egbert Rijke (May 14 2020 at 10:07):

Wouldn't Floris be the right man for this job? He knows HoTT, he knows Lean, he knows basically everything and he's fast

view this post on Zulip Mario Carneiro (May 14 2020 at 10:09):

That's a good question. @Floris van Doorn ? My impression was that his work is primarily "internal HoTT" and yours is "external HoTT", but correct me if not

view this post on Zulip Egbert Rijke (May 14 2020 at 10:11):

I'm doing mainly synthetic homotopy theory, so similar to Floris. But my flaw is that I really struggle with Lean.

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

I think the introduction to https://arxiv.org/abs/1411.1736 has explained to me what is going on in https://arxiv.org/abs/1406.3219v4

view this post on Zulip Mario Carneiro (May 14 2020 at 10:13):

I've been pushing for informal mathematicians to contribute to formalization more in the area of "formal roadmaps", where things are laid out precisely and at a fairly low sophistication, but not formally, with others picking up the remainder

view this post on Zulip Mario Carneiro (May 14 2020 at 10:13):

that seems to me to be a good division of labor

view this post on Zulip Egbert Rijke (May 14 2020 at 10:15):

I'll be back in an hour or two

view this post on Zulip Reid Barton (May 14 2020 at 10:15):

Do we have the syntax of MLTT formalized somewhere?

view this post on Zulip Reid Barton (May 14 2020 at 10:15):

Possibly not in Lean?

view this post on Zulip Mario Carneiro (May 14 2020 at 10:16):

do PTSs count?

view this post on Zulip Reid Barton (May 14 2020 at 10:18):

I don't know. Something that has contexts, types and terms at least.

view this post on Zulip Reid Barton (May 14 2020 at 10:20):

I guess that Agda formalization from earlier must.

view this post on Zulip Reid Barton (May 14 2020 at 10:22):

https://github.com/guillaumebrunerie/initiality/blob/reflection/typetheory.agda
https://github.com/guillaumebrunerie/initiality/blob/reflection/syntx.agda

view this post on Zulip Reid Barton (May 14 2020 at 10:25):

oh, and
https://github.com/guillaumebrunerie/initiality/blob/reflection/rules.agda

view this post on Zulip Reid Barton (May 14 2020 at 10:27):

does this look like a good starting point, if we removed all the formers we don't want to handle?

view this post on Zulip Mario Carneiro (May 14 2020 at 10:44):

Here's a sketch:

import tactic

inductive exp : Type
| nat
| prod : exp  exp  exp
| sum : exp  exp  exp
| var :   exp
| app : exp  exp  exp
| lam : exp  exp  exp
| pi : exp  exp  exp

def exp.subst : exp  exp  exp := sorry

inductive pf_kind : Type
| type : exp  option exp  pf_kind
| defeq : exp  exp  option exp  pf_kind
open pf_kind

def is_type (e) := type e none

inductive pf : list exp  pf_kind  Prop
| nat {Γ} : pf Γ (is_type exp.nat)
| prod {Γ A B} : pf Γ (is_type A)  pf Γ (is_type B)  pf Γ (is_type (exp.prod A B))
| sum {Γ A B} : pf Γ (is_type A)  pf Γ (is_type B)  pf Γ (is_type (exp.sum A B))
| var {Γ n A} : list.nth Γ n = some A  pf Γ (type (exp.var n) A)
| app {Γ A f e B} : pf Γ (is_type A)  pf (A :: Γ) (is_type B) 
  pf Γ (type f (exp.pi A B))  pf Γ (type e A) 
  pf Γ (type (exp.app f e) (exp.subst e B))
| lam {Γ A e B} : pf Γ (is_type A)  pf (A :: Γ) (type e B) 
  pf Γ (type (exp.lam A e) (exp.pi A B))
| pi {Γ A B} : pf Γ (is_type A)  pf (A :: Γ) (is_type B)  pf Γ (is_type (exp.pi A B))
| defeq {Γ A e B} : pf Γ (defeq A B none)  pf Γ (type e A)  pf Γ (type e B)
| refl {Γ e A} : pf Γ (type e A)  pf Γ (defeq e e A)
| symm {Γ s t A} : pf Γ (defeq s t A)  pf Γ (defeq t s A)
| trans {Γ s t u A} : pf Γ (defeq s t A)  pf Γ (defeq t u A)  pf Γ (defeq s u A)
| prod_eq {Γ A₁ B₁ A₂ B₂} :
  pf Γ (defeq A₁ B₁ none)  pf Γ (defeq A₂ B₂ none) 
  pf Γ (defeq (exp.prod A₁ B₁) (exp.prod A₂ B₂) none)
| sum_eq {Γ A₁ B₁ A₂ B₂} :
  pf Γ (defeq A₁ B₁ none)  pf Γ (defeq A₂ B₂ none) 
  pf Γ (defeq (exp.sum A₁ B₁) (exp.sum A₂ B₂) none)
| lam_eq {Γ A s t B} :
  pf Γ (is_type A)  pf (A :: Γ) (defeq s t B) 
  pf Γ (defeq (exp.lam A s) (exp.lam A t) (exp.pi A B))
| pi_eq {Γ A s t} :
  pf Γ (is_type A)  pf (A :: Γ) (defeq s t none) 
  pf Γ (defeq (exp.pi A s) (exp.pi A t) none)
| beta {Γ A e₁ e₂ B} :
  pf Γ (is_type A)  pf (A :: Γ) (type e₁ B)  pf Γ (type e₂ A) 
  pf Γ (defeq (exp.app (exp.lam A e₁) e₂) (exp.subst e₂ e₁) (option.map (exp.subst e₂) B))

view this post on Zulip Sarah Reboullet (May 14 2020 at 11:22):

I kind of came late to the party but have you considered using a thing like Orton and Pitts' axioms for Cubical Type Theory ( https://arxiv.org/abs/1712.04864 ) to get an axiomatic HoTT in a theory that may have axiom K? (Because as Jannis Limperg rightly said this is the issue with Lean and axiomatic HoTT.) I did that in a previous intership to get a model of HoTT inside a MLTT with extensional identity and do weird HoTT stuff with it. I guess this is what is done in Coq in https://gitlab.inria.fr/sboulier/thesis-formalizations/-/tree/master/InternalCubical-Coq . From a theoretical point of view I think (even it I haven't saw any paper about it) it makes your meta-theory into a 2 level type theory with both univalent identities and universes and "regular" (with axiom K) identities and universes. I think that those doing Synthetic Homotopy Theory like this because it's them that introduces this kind of notions ... (It's even Voevodsky who introduces first 2-level TT according to n-lab.)

view this post on Zulip Mario Carneiro (May 14 2020 at 11:24):

well, the hope here is to have a completely non-univalent/classical metatheory consistent with standard mathematical practice, rather than a two level metatheory (which requires special features in the kernel)

view this post on Zulip Sarah Reboullet (May 14 2020 at 11:30):

Yes, I agree. Orton and Pitts' method doesn't require a change in kernel (that's the point of their method), but only the adding of axioms (or a typeclass for the axioms). As such you still have a classical with-K metatheory as is Lean. But I understand if this isn't satisfactory. I just wondered.

view this post on Zulip Reid Barton (May 14 2020 at 11:42):

Maybe we should move this discussion about models of MLTT to another topic.

view this post on Zulip Floris van Doorn (May 14 2020 at 19:40):

I haven't read the whole discussion, but some comments:

  • I believe a big reason that people doing HoTT want their models constructive is so that they can replay the proof in a topos. For example, if you make a model internal to a realizability topos, you can get a model of HoTT with an impredicative univalent universe (i.e. a universe that is closed under Pi (x : A), B x where A might live in a larger universe). See for example http://www.mat.uc.pt/~ct2017/slides/frey_j.pdf
  • I also think that the fact that the cubical model is constructive is used for writing down explicitly the rules for cubical type theory, the reduction rules for the composition operator are based on the equalities in the model. I don't know the details here.
  • "Formalizing HoTT" is an open-ended problem: what type-formers do you have? Pi and Sigma probably, but inductive types? which higher inductive types? Also, there are many different models, so there are many choices there, too
  • It is an interesting project, but I believe I have seen projects on Github trying to already do exactly this in other proof assistants. I cannot find them now though, and I don't remember much more (I think it was in Coq?)
  • Also interesting might be the Initiality Project, a non-formal but detailed crowsourced project with the aim to prove that the syntactic model is initial is some precise sense. It doesn't look very alive though: https://ncatlab.org/nlab/show/Initiality+Project

view this post on Zulip Floris van Doorn (May 14 2020 at 21:53):

I think this is the repository I was looking for: https://github.com/guillaumebrunerie/initiality
This is formalizing the initiality conjecture, which in particular requires formalizing categorical models of the type theory. It is not completely clear to me if this is HoTT or MLTT...

view this post on Zulip Reid Barton (May 15 2020 at 20:26):

Yes, we discussed this repository some in the other thread. I think the framework they use (contextual categories) applies to both intensional and extensional MLTT.

view this post on Zulip Reid Barton (May 15 2020 at 20:27):

However, they don't actually construct any examples of contextual categories (besides the initial one, the term model) and this actually seems like quite a lot of work, and one still has to solve a coherence problem somehow

view this post on Zulip Reid Barton (May 15 2020 at 20:28):

For instance it would be nice to prove that Type is a model of MLTT at least.

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

Regarding constructivity: there seems to be a considerable amount of work needed on the type theory side, which does not depend on the particular model, and which is presumably constructive. So it could make sense to first construct a model classically, and then when the rest of the system is in place, upgrade it to one built constructively.

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

Regarding which type formers (and rules) to include: I would say start small, but to claim to be a model of HoTT, one should at least be able to state the univalence axiom (and then check that it is true in the model).

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

I'm not sure the model theory of higher inductive types has even been worked out mathematically yet, so I would exclude those to start for sure.

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

(By the "model theory" I mean specifically the problem of constructing a model with all the necessary structure)

view this post on Zulip Valery Isaev (May 16 2020 at 13:33):

Reid Barton said:

I'm not sure the model theory of higher inductive types has even been worked out mathematically yet, so I would exclude those to start for sure.

I think the best we have is https://arxiv.org/abs/1705.07088, which gives a large class of models of a large class of HITs.

view this post on Zulip Reid Barton (May 16 2020 at 20:06):

Thanks. So near the end of the introduction, they write that their method does not yield universes that are closed under the construction of higher inductive types. That would be a problem for interpreting something like book HoTT, right? Do you know whether this is still an open problem?

view this post on Zulip Valery Isaev (May 16 2020 at 20:59):

I don't know. Better ask on the HoTT chat.


Last updated: May 08 2021 at 22:13 UTC