## Stream: Type theory

### Topic: How to get HoTT people into Lean

#### 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?

#### 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

#### 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

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

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

#### 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"

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

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

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

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

#### 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

#### 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

#### 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.

#### 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

#### 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)

#### 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

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

so it's not really a decision you can defer

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

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

#### 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)

#### 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.

#### 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.)

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

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

#### 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

#### 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

#### 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.

#### 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

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

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

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

can someone unpack that quote for me?

#### 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)

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

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

#### 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.

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

what do you mean by "deeply embed"?

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

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

#### 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

#### 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

#### 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".

#### 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"?

#### 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"?

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

It would be impractical without a lot of automation.

#### 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.

#### 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.

ah interesting

#### 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"

#### 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

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

Definitely from scratch

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

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

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

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

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

Not least because it has already been done for you

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

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

#### 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

#### 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)

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

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

(deleted)

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

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

#### 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?

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

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

#### 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

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

I can't parse that last sentence

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

if you were responding to me, is that better?

#### 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.

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

I don't wish lean world domination at equilibrium

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

you can't have tools without communities to maintain them

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

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

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

But we can change these answers independently.

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

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

#### 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.

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

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

#### 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

Or vice versa.

okay

#### Mario Carneiro (May 13 2020 at 20:00):

which isn't too far from current reality

#### Mario Carneiro (May 13 2020 at 20:01):

(except for the mutually interpretable part)

#### 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.

#### 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

details

#### 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

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

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

#### 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

#### 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)

that's fine

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

what is interpretability up to extra axioms?

#### 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

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

does it allow for "automated translations"?

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

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

#### Mario Carneiro (May 13 2020 at 20:05):

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

#### 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

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

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

#### Mario Carneiro (May 13 2020 at 20:05):

A spanning tree has no designated root

#### Mario Carneiro (May 13 2020 at 20:06):

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

#### 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

#### 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

#### Mario Carneiro (May 13 2020 at 20:07):

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

#### 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

#### Mario Carneiro (May 13 2020 at 20:07):

(most are trivial because they are actually definitions)

#### 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

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

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

#### Mario Carneiro (May 13 2020 at 20:09):

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

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

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

#### Mario Carneiro (May 13 2020 at 20:09):

it generally can't be automated

#### 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?

#### 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

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

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

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

by apply_instance?

#### 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

#### 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

#### 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?

right

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

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

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

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

#### 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

#### Mario Carneiro (May 13 2020 at 20:14):

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

#### 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

#### 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

#### 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

#### Mario Carneiro (May 13 2020 at 20:18):

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

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

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

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

I see @Egbert Rijke in the chat...

#### Egbert Rijke (May 13 2020 at 22:19):

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.

#### 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?

#### Reid Barton (May 13 2020 at 22:21):

No, certainly not

#### 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

#### 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?

#### 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.

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

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

#### 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

#### 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.

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

Do we have topoi yet?

#### Reid Barton (May 13 2020 at 22:29):

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

#### Reid Barton (May 13 2020 at 22:29):

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

#### Reid Barton (May 13 2020 at 22:29):

If the README is up to date then "soon"

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

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

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

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

#### 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

#### Bhavik Mehta (May 13 2020 at 22:30):

Actually the readme is a bit out of date

#### 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

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

where do dependent pis come from?

#### Bhavik Mehta (May 13 2020 at 22:31):

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

#### Bhavik Mehta (May 13 2020 at 22:32):

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

#### 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

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

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

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

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

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

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

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

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

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

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

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

the empty perfectoid space of HoTT

perfect

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

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

#### Reid Barton (May 13 2020 at 22:37):

Otherwise it should, yes

#### 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.

#### 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

#### 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

#### Reid Barton (May 13 2020 at 22:40):

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

#### 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

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

that sounds right

#### 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

#### Reid Barton (May 13 2020 at 22:41):

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

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

oh, I think I see the issue

#### Reid Barton (May 13 2020 at 22:42):

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

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

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

#### Bhavik Mehta (May 13 2020 at 22:42):

Reid Barton said:

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

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

#### 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'' \to \Gamma$ whether you did it in one step or two

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

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

#### Reid Barton (May 13 2020 at 22:43):

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

#### Bhavik Mehta (May 13 2020 at 22:43):

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

#### Reid Barton (May 13 2020 at 22:43):

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

#### 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 "$\Gamma \vdash A\,\mathrm{prop}$" and this is modelled by a subobject

#### 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

#### 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.

#### 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?

#### 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)

#### 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.

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

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

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

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

#### 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 "$\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

#### 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

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

does the elephant cover dependent type theory?

#### Bhavik Mehta (May 13 2020 at 22:51):

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

#### Bhavik Mehta (May 13 2020 at 22:52):

It does talk about MLTT though in D4.4

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

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

#### 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

#### 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

#### Reid Barton (May 13 2020 at 23:00):

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

#### 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.

#### 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.

#### 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.

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

Mario Carneiro said:

does the elephant cover dependent type theory?

Sorry it does!

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

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

#### 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

#### Mario Carneiro (May 13 2020 at 23:17):

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

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

I mean two contexts which you can permute

I think

#### Mario Carneiro (May 13 2020 at 23:18):

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

#### 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?

#### Mario Carneiro (May 13 2020 at 23:21):

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

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

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

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

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

#### 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?

#### 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?

#### 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

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

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

#### 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

#### Mario Carneiro (May 13 2020 at 23:31):

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

no mbox :frown:

image.png

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

image.png this precedes Def 4.4.3

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

Oh I see, $MB$ is actually abuse of notation

#### 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

#### Reid Barton (May 13 2020 at 23:53):

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

#### Mario Carneiro (May 13 2020 at 23:58):

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

#### Reid Barton (May 13 2020 at 23:58):

I like the last line of the conclusion

#### 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

#### 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

#### 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

#### 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

#### Mario Carneiro (May 14 2020 at 00:03):

agda users do seem to like to build everything from scratch

#### Reid Barton (May 14 2020 at 00:03):

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

#### Reid Barton (May 14 2020 at 00:04):

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

#### Mario Carneiro (May 14 2020 at 00:04):

oh, ft stands for father

#### Reid Barton (May 14 2020 at 00:05):

oh that makes more sense than "foot"

#### Mario Carneiro (May 14 2020 at 00:06):

does anyone want to try transcribing CCat in lean?

no

#### Mario Carneiro (May 14 2020 at 00:09):

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

#### Reid Barton (May 14 2020 at 00:09):

It's just ... really long

#### 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

#### Bhavik Mehta (May 14 2020 at 00:10):

at least a third of it just looks like category axioms

#### Mario Carneiro (May 14 2020 at 00:11):

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

ah

#### Mario Carneiro (May 14 2020 at 00:11):

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

#### Reid Barton (May 14 2020 at 00:21):

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

#### Reid Barton (May 14 2020 at 00:22):

then the associated contextual category has

• as objects, for each $n$, strings $X_n \to \cdots \to X_1 \to X_0 = *$
• as morphisms from $X_n \to \cdots \to X_1 \to X_0 = *$ to $Y_m \to \cdots \to Y_1 \to Y_0 = *$, just maps $X_n \to Y_m$

#### Reid Barton (May 14 2020 at 00:26):

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

#### 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₁


#### 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'' \to \Gamma$ whether you did it in one step or two

#### Reid Barton (May 14 2020 at 00:29):

where:

• X is $A$
• Z is $\Gamma$
• Y is $\Gamma'$
• the unnamed source of f is $\Gamma''$

#### 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.

#### 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₀)


#### Mario Carneiro (May 14 2020 at 00:33):

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

#### Reid Barton (May 14 2020 at 00:34):

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

#### 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?)

#### 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

#### 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

#### 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

#### Mario Carneiro (May 14 2020 at 00:46):

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

#### 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.

#### 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.

#### 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".

#### Mario Carneiro (May 14 2020 at 00:50):

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

#### 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

#### 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.

#### 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

#### Mario Carneiro (May 14 2020 at 09:51):

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

#### Mario Carneiro (May 14 2020 at 09:51):

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

#### Mario Carneiro (May 14 2020 at 09:55):

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

#### 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?

#### Mario Carneiro (May 14 2020 at 09:55):

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

#### 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

#### Reid Barton (May 14 2020 at 09:56):

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

#### Egbert Rijke (May 14 2020 at 09:56):

Ok, then I assume that you have all you need

#### Johan Commelin (May 14 2020 at 09:57):

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

#### 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

#### Mario Carneiro (May 14 2020 at 09:57):

possibly reid or bhavik can fill that role

#### Mario Carneiro (May 14 2020 at 09:58):

Certainly you can, if you are willing

#### Mario Carneiro (May 14 2020 at 10:02):

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

#### 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

#### 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

#### 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.

#### 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

#### 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

#### Mario Carneiro (May 14 2020 at 10:13):

that seems to me to be a good division of labor

#### Egbert Rijke (May 14 2020 at 10:15):

I'll be back in an hour or two

#### Reid Barton (May 14 2020 at 10:15):

Do we have the syntax of MLTT formalized somewhere?

#### Reid Barton (May 14 2020 at 10:15):

Possibly not in Lean?

do PTSs count?

#### Reid Barton (May 14 2020 at 10:18):

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

#### Reid Barton (May 14 2020 at 10:20):

I guess that Agda formalization from earlier must.

#### 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?

#### 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))


#### 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.)

#### 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)

#### 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.

#### Reid Barton (May 14 2020 at 11:42):

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

#### Floris van Doorn (May 14 2020 at 19:40):

• 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

#### 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...

#### 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.

#### 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

#### 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.

#### 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.

#### 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).

#### 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.

#### 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)

#### 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.

#### 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?

#### 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