How to get HoTT people into Lean

Stream: Type theory

[Jalex Stark]

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

[Bhavik Mehta]

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]

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]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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]

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]

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]

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

[Reid Barton]

so it's not really a decision you can defer

[Reid Barton]

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

[Bhavik Mehta]

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?

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Jalex Stark]

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]

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

can someone unpack that quote for me?

[Jalex Stark]

(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]

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

[Jannis Limperg]

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]

what do you mean by "deeply embed"?

[Jalex Stark]

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

[Bhavik Mehta]

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]

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]

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

[Jalex Stark]

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

[Jalex Stark]

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]

It would be impractical without a lot of automation.

[Reid Barton]

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]

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.

[Jalex Stark]

ah interesting

[Jalex Stark]

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]

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]

Definitely from scratch

[Jalex Stark]

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

[Mario Carneiro]

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

[Reid Barton]

Not least because it has already been done for you

[Reid Barton]

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

[Mario Carneiro]

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]

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]

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

[Jalex Stark]

(deleted)

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

I can't parse that last sentence

[Jalex Stark]

if you were responding to me, is that better?

[Reid Barton]

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

[Mario Carneiro]

I don't wish lean world domination at equilibrium

[Jalex Stark]

you can't have tools without communities to maintain them

[Jalex Stark]

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

[Reid Barton]

But we can change these answers independently.

[Jalex Stark]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

Or vice versa.

[Jalex Stark]

okay

[Mario Carneiro]

which isn't too far from current reality

[Mario Carneiro]

(except for the mutually interpretable part)

[Reid Barton]

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]

Mario Carneiro said:

which isn't too far from current reality

Well... and that part about world domination

[Mario Carneiro]

details

[Jalex Stark]

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]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

that's fine

[Jalex Stark]

what is interpretability up to extra axioms?

[Mario Carneiro]

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

[Jalex Stark]

does it allow for "automated translations"?

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

A spanning tree has no designated root

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Jalex Stark]

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]

(most are trivial because they are actually definitions)

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

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

[Jalex Stark]

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

[Mario Carneiro]

it generally can't be automated

[Jalex Stark]

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

[Mario Carneiro]

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]

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

[Jalex Stark]

by apply_instance?

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

right

[Jalex Stark]

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

[Jalex Stark]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Jalex Stark]

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

[Mario Carneiro]

I see @Egbert Rijke in the chat...

[Egbert Rijke]

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.

[Mario Carneiro]

@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]

No, certainly not

[Mario Carneiro]

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

[Mario Carneiro]

@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]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

Do we have topoi yet?

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

If the README is up to date then "soon"

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

Actually the readme is a bit out of date

[Bhavik Mehta]

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

[Mario Carneiro]

where do dependent pis come from?

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

the empty perfectoid space of HoTT

[Mario Carneiro]

perfect

[Mario Carneiro]

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

[Reid Barton]

Otherwise it should, yes

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

that sounds right

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

oh, I think I see the issue

[Reid Barton]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

does the elephant cover dependent type theory?

[Bhavik Mehta]

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

[Bhavik Mehta]

It does talk about MLTT though in D4.4

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

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]

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]

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]

Mario Carneiro said:

does the elephant cover dependent type theory?

Sorry it does!

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

I mean two contexts which you can permute

[Bhavik Mehta]

I think

[Mario Carneiro]

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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]

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?

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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$

[Reid Barton]

no mbox :frown:

[Bhavik Mehta]

image.png

[Bhavik Mehta]

image.png this precedes Def 4.4.3

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Reid Barton]

I like the last line of the conclusion

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

agda users do seem to like to build everything from scratch

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

oh, ft stands for father

[Reid Barton]

oh that makes more sense than "foot"

[Mario Carneiro]

does anyone want to try transcribing CCat in lean?

[Reid Barton]

no

[Mario Carneiro]

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

[Reid Barton]

It's just ... really long

[Mario Carneiro]

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]

at least a third of it just looks like category axioms

[Mario Carneiro]

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

[Bhavik Mehta]

ah

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

where:

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Mario Carneiro]

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

[Egbert Rijke]

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.

[Egbert Rijke]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

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]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Egbert Rijke]

Ok, then I assume that you have all you need

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

possibly reid or bhavik can fill that role

[Mario Carneiro]

Certainly you can, if you are willing

[Mario Carneiro]

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

[Egbert Rijke]

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]

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]

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

[Reid Barton]

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]

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]

that seems to me to be a good division of labor

[Egbert Rijke]

I'll be back in an hour or two

[Reid Barton]

Do we have the syntax of MLTT formalized somewhere?

[Reid Barton]

Possibly not in Lean?

[Mario Carneiro]

do PTSs count?

[Reid Barton]

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

[Reid Barton]

I guess that Agda formalization from earlier must.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Floris van Doorn]

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

[Floris van Doorn]

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]

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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Valery Isaev]

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]

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]

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