HoTT

Stream: maths

[Kevin Buzzard]

Here's a message I just posted to the homotopy type theory google group forum:

Hi from a Lean user.

As many people here will know, Tom Hales' formal abstracts project https://formalabstracts.github.io/ wants to formalise many of the statements of modern pure mathematics in Lean. One could ask more generally about a project of formalising many of the statements of modern pure mathematics in an arbitrary system, such as HoTT. I know enough about the formalisation process to know that whatever system one chooses, there will be pain points, because some mathematical ideas fit more readily into some foundational systems than others.

I have seen enough of Lean to become convinced that the pain points would be surmountable in Lean. I have seen enough of Isabelle/HOL to become skeptical about the idea that it would be suitable for all of modern pure mathematics, although it is clearly suitable for some of it; however it seems that simple type theory struggles to handle things like tensor products of sheaves of modules on a scheme, because sheaves are dependent types and it seems that one cannot use Isabelle's typeclass system to handle the rings showing up in a sheaf of rings.

I have very little experience with HoTT. I have heard that the fact that "all constructions must be isomorphism-invariant" is both a blessing and a curse. However I would like to know more details. I am speaking at the Big Proof conference in Edinburgh this coming Wednesday on the pain points involved with formalising mathematical objects in dependent type theory and during the preparation of my talk I began to wonder what the analogous picture was with HoTT.

Everyone will have a different interpretation of "modern pure mathematics" so to fix our ideas, let me say that for the purposes of this discussion, "modern pure mathematics" means the statements of the theorems publishsed by the Annals of Mathematics over the last few years, so for example I am talking about formalising statements of theorems involving L-functions of abelian varieties over number fields, Hodge theory, cohomology of algebraic varieties, Hecke algebras of symmetric groups, Ricci flow and the like; one can see titles and more at http://annals.math.princeton.edu/2019/189-3 . Classical logic and the axiom of choice are absolutely essential -- I am only interested in the hard-core "classical mathematician" stance of the way mathematics works, and what it is.

If this is not the right forum for this question, I would be happily directed to somewhere more suitable. After spending 10 minutes failing to get onto ##hott on freenode ("you need to be identified with services") I decided it was easier just to ask here. If people want to chat directly I am usually around at https://leanprover.zulipchat.com/ (registration required, full names are usually used, I'll start a HoTT thread in #mathematics).

Kevin Buzzard

Does anyone here have enough experience with HoTT to say anything? I've asked here questions like "what would the pain points be if one tried to formalise a scheme in HoTT?" and have got answers of the form "if you want to find out, you should go ahead and try". I'm not sure I have time to learn another system though. I have even dumber questions -- how would one define the trace of a linear map from a finite-dimensional vector space to itself? A mathematician would pick a basis, compute the trace of the corresponding matrix, and then note that it was independent of the choice. Is this problematic in HoTT?

[Reid Barton]

I suppose it will depend on exactly how you define "finite-dimensional vector space". If it's defined as a vector space together with trunc of a basis, then the procedure for defining the trace of a map goes exactly how you describe.

[Reid Barton]

trunc is called the "propositional truncation" in HoTT although "proposition" there more closely corresponds to what Lean calls subsingleton

[Reid Barton]

In particular, this definition is constructive. However you would probably need the axiom of choice to prove that a quotient of a finite dimensional vector space is again finite dimensional.

[Reid Barton]

Or maybe LEM is enough, but that's still an uncomputable axiom

[Reid Barton]

I haven't actually used a HoTT-based theorem prover yet, only read the book. I do find it difficult to get a sense of how HoTT+choice would work in practice. I think this is a cultural phenomenon: there tends to be overlap between people interested in HoTT and people interested in constructive logic. (Consider that the same could be said about Coq, yet Lean is based on essentially the same underlying type theory and look where we are now.)

[Reid Barton]

@Floris van Doorn Does the construction of the Serre SS use any axioms?

[Reid Barton]

Kevin, I wouldn't be surprised if in fact nobody has done anything resembling what you're asking about.

[Reid Barton]

In the areas that require classical logic/choice, I mean.

[Mario Carneiro]

I think UniMath is trying to build a general mathematical library on a HoTT foundation

[Mario Carneiro]

I think it slowed down when Voevodsky died though

[Kevin Buzzard]

What am I asking about? Doing fabstracts in hott or making schemes in hott? I am currently thinking about undergraduate maths. Say V and W are finite dimensional vector spaces over an arbitrary field, defined however you like, and we have a linear map from V to W. Say X is the kernel. Say I have a linear map from X to X. Can I define its trace in HoTT?

[Kevin Buzzard]

So unimath is to mathlib as hott is to lean?

[Mario Carneiro]

I think so, I'm no expert though

[Kevin Buzzard]

Then where is the analogue of me who tried to do completely dumb simple maths things in HoTT?

[Mario Carneiro]

I certainly wouldn't be able to answer that

[Mario Carneiro]

I'm sure there are such people in the community but I'm not enough a part of it to say

[Kevin Buzzard]

Can it be done and how far did they get? Where are the pain points? Who should I ask?

[Mario Carneiro]

I guess the UniMath foundation?

[Kevin Buzzard]

Hopefully someone will respond to my post on the mailing list

[Kevin Buzzard]

Thanks, I'll try them

[Mario Carneiro]

Part of the problem is that the HoTT world is very fragmented, so no individual project has very many people working on it

[Mario Carneiro]

which I might argue is one of the downsides of DTT, strangely enough

[Mario Carneiro]

The HoTT people really embrace the D in DTT, and when you work like that the exact details of definitional equality matter a lot; but there is not a uniform conception of what it should be, so you end up with a bunch of incompatible axiomatizations

[Kevin Buzzard]

Does unimath work only with constructive maths??

[Kevin Buzzard]

No such system will ever catch on with mathematicians

[Mario Carneiro]

The axioms accepted are: the univalence axiom, the law of excluded middle, the axiom of choice, and a few new variants of the axiom of choice, validated by the semantic model.

[Kevin Buzzard]

I am continually weirded out by the fact that Leo simultaneously seems completely uninterested in mathematics and yet seems to have made the system which is most suitable for general pure mathematicians

[Kevin Buzzard]

Ok great I'll ask the univalent people if they can define the trace of a linear map and a scheme

[Mario Carneiro]

I heard about it from Daniel Grayson, who is the lead developer; you could ask him for a summary

[Kevin Buzzard]

Oh I know Dan from my sci.math.research days

[Mario Carneiro]

the readme at https://github.com/UniMath/UniMath/tree/master/UniMath has a bunch of useful general info

[Reid Barton]

What am I asking about? Doing fabstracts in hott or making schemes in hott? I am currently thinking about undergraduate maths. Say V and W are finite dimensional vector spaces over an arbitrary field, defined however you like, and we have a linear map from V to W. Say X is the kernel. Say I have a linear map from X to X. Can I define its trace in HoTT?

I mean formalizing even relatively basic constructions like this one that (apparently) require choice.
I'm pretty sure that this is possible in HoTT (plus choice). In either HoTT or Lean you must first prove that X is finite dimensional (has a finite basis); that part will go the same way. In HoTT you will also need to prove that the trace is independent of the choice of basis, which is not a bad thing.

[Kevin Buzzard]

In HoTT if I define what it means for a ring to be local, would I have to prove that a ring isomorphic to a local ring is local before I can even make the definition?

[Reid Barton]

No, you'd define it the same way as in Lean

[Chris Hughes]

I think even stupid thing like this are isomorphism invariant in HoTT.

example {α : Type} [ring α] : Prop :=
∃ h : ℤ = α, (0 : α) = eq.rec_on h 37

[Reid Barton]

I think a first approximation to how choice works in HoTT, expressed in the language of Lean, is that one can no longer have choice : nonempty X -> X, but one still has

• unique_choice : nonempty X -> trunc X, which means that you can extract a witness for an existential to construct something provided you can prove the result doesn't depend on the choice of witness, and
• axiom_of_choice : (∀ x, ∃ y, r x y) -> ∃ f, ∀ x, r x (f x)

[Chris Hughes]

What's the difference between nonempty and trunc in HoTT?

[Reid Barton]

There isn't one (at least in book HoTT) because HoTT has no notion of judgmentally being a proposition.

[Chris Hughes]

So unique choice is id?

[Reid Barton]

So the result is that places where we would use an ∃ in Lean correspond to || ∃ ... || in HoTT

[Reid Barton]

or let's say || Σ ... || to be more clear

[Reid Barton]

where || ... || is the propositional truncation (Lean trunc)

[Reid Barton]

Right, so unique choice doesn't really correspond to anything in HoTT but I tried to give a translation into a Lean worldview.

[Reid Barton]

Actually the HoTT book does have something it calls "unique choice", which is the statement that if P is a Prop (Lean: subsingleton P) then P is equivalent to ||P||.

[Reid Barton]

But it's a theorem

[Kevin Buzzard]

Is UniMath written in book HoTT?

[Reid Barton]

"Close enough"

[Reid Barton]

It seems to be book HoTT minus some features like inductive types

[Kevin Buzzard]

So given a tool like Coq or Lean, you can either use it as God intended, as it were, or you can start adding additional rules of the form "you can use this axiom" and "you can't use this command"

[Kevin Buzzard]

This then surely makes for a more inefficient system, as the way it is designed is somehow slightly in conflict with the way it is being used.

[Koundinya Vajjha]

Here's my two cents:
The main advantage univalence gives us from a formalization perspective is that it allows for implementation irrelevance. I can build an entire library of the p-adics using the algebraic definition, and if someone in the future needs to use the analytic definition, she can simply transport the statements (and proofs!) proven using the first definitions onto the second.

[Koundinya Vajjha]

However, this requires computable univalence, which is an open problem in book HoTT.

[Koundinya Vajjha]

If we do "fabstracts in HoTT", then it would mean that we could formalize a single definition for each mathematical statement and that would, by univalence, be akin to formalizing a whole equivalence class of such definitions. (upto homotopy)

[Koundinya Vajjha]

Sadly this would require changes to the underlying type theory to one where univalence actually computes, such as cubical type theory.

[Kevin Buzzard]

Here's my two cents:
The main advantage univalence gives us from a formalization perspective is that it allows for implementation irrelevance. I can build an entire library of the p-adics using the algebraic definition, and if someone in the future needs to use the analytic definition, she can simply transport the statements (and proofs!) proven using the first definitions onto the second.

I don't see any reason why we can't do this in Lean, once those computer scientists have written the transport tactic for us.

[Koundinya Vajjha]

I haven't used transport so I don't know how it works. But I would conjecture that it isn't as powerful as full univalence. (In what sense exactly, I don't know)
But people have tried to get Univalent parametricity without changing the type theory: https://hal.inria.fr/hal-01559073

[Mario Carneiro]

I think that untyped set theory is much better at "implementation invariance" than dependent type theory, in general

[Mario Carneiro]

In DTT all your definitions can potentially be "unfolded" and this might matter for making some terms type correct, if they appear as dependencies in a type

[Mario Carneiro]

so you basically can't really hide anything, at least in principle

[Mario Carneiro]

Whether transport is as powerful as full univalence is actually an open research question. It's related to whether univalence computes "propositionally" in book HoTT

[Kevin Buzzard]

I still don't really understand how Strickland's idea managed to get the schemes project out of the hole I'd dug it into.

[Floris van Doorn]

I'm late to the party, but here are some of my responses.

Does the construction of the Serre SS use any axioms?

No, only univalence and higher inductive types. In HoTT there is a very strong sense of "trying to avoid the axiom of choice". And if you care about that (which mathematicians of course don't), there are some nice new things you can do with HoTT to avoid axioms:

• You can elimination from the propositional truncation (which is like nonempty) to any subsingleton type without using an axiom. In Lean you would use choice for this.
• Normally, if you define the real numbers as Cauchy sequences, you need the (countable) axiom of choice to prove completeness of the real numbers. In HoTT there is a definition of the Cauchy real numbers as a higher inductive type where you can prove completeness without the axiom of choice (you still need choice to prove that it is equivalent to the Dedekind real numbers).

This is not to say you cannot add the axiom of choice to HoTT and work classically. This is very much possible. However, as Reid mentions you cannot add classical.choice (that is inconsistent with univalence), you need the weaker set-theoretic formulation of choice (e.g. every surjection has a section).

[Floris van Doorn]

what would the pain points be if one tried to formalise a scheme in HoTT?

I think the pain points much more depend on which proof assistant you use, and more importantly: which tactics and automation is available. One example of a pain point when doing HoTT in Lean 2 which are specific to HoTT, is that - for example - I had to prove that the ordering on the natural numbers is a proposition (subsingleton): https://github.com/leanprover/lean2/blob/master/hott/types/nat/hott.hlean#L14

definition is_prop_le [instance] (n m : ℕ) : is_prop (n ≤ m)

A much bigger pain point is that univalence doesn't compute in Lean 2, so if you want a function you define to compute definitionally (and in Lean 2 we wanted that, partially because of the lack of a good simp), then you want to avoid using univalence. This made me define many many concepts explicitly which I could have defined using univalence.

[Floris van Doorn]

One mentality problem in HoTT is that everything - even proofs of propositions - are definitions and it sometimes matters how you define/prove them, especially if you use dependent types heavily. For example, if you have a sequence of maps X 0 -> X 1 -> X 2 -> ... then you can define a function n <= m -> X n -> X m. In HoTT you can define this function by recursion on the proof that n <= m, and so how that function computes depends on how you have proven that n <= m (for numerals n and m there is only 1 way to do this, but for variables there could be different ways, of course). At one point, I reproved some inequalities of natural numbers to make this function compute better (and it was important that it computed better because I was using dependent types).

[Andrew Ashworth]

Out of curiosity, does anyone know about how usable cubical type theory is?

[Floris van Doorn]

What do you mean by usable?

• Usable for doing HoTT? Yes, although most proof assistants implementing univalence are pretty experimental and lack high-level features.
• Usable for computation of univalence? Yes, it can compute univalence. Although with complicated proofs, the computation is inefficient, so you will have to optimize your proof for efficient computation.
• Usable for doing ordinary mathematics? Probably not really.

[Kevin Buzzard]

You mean for the cubing a cube question? ;-)

[Kevin Buzzard]

https://groups.google.com/forum/#!topic/homotopytypetheory/NhIhMd7SM_4

The discussion on the HoTT mailing list says a bunch of things which many people here knew already; I guess they are slowly but surely dawning on me.

[Johan Commelin]

It seems that HoTT and UniMath find it very important that everything is constructive and computable. Are their p-adics computable?

[Kevin Buzzard]

The p-adics are uncountable so it's not even clear, I think, what this question can mean.

[Rob Lewis]

Their paper says their p-adics are constructive. One way to interpret the computability question is to ask if they can define computable functions on the p-adics. For example, given a closed term of Z_p you might want to compute its norm. As far as I could tell, they don't define any functions beyond the arithmetic ones, computably or noncomputably. And univalence doesn't compute in UniMath. That may or may not show up to block things here, I don't know.

[Kevin Buzzard]

A quote from (page 1 of) @Floris van Doorn 's thesis:

The fact that all constructions are homotopy invariant also leads to some challenges.
It is not always clear whether we can define a concept of homotopy theory in homotopy
type theory. For example, singular homology is a homotopy invariant notion, but in the
construction we use the set of all simplices in a space, which is not a homotopy invariant
notion. In this case, we can define homology in a different way (see Section 5.5).
However, for other definitions, such as the Grassmannian manifolds, it is an open
problem whether they can be constructed in homotopy type theory.

Wait--what? Are we just talking about the standard smooth projective varieties of e.g. subspaces of a f.d. vector space? What is the trouble with making them in HoTT?

[Reid Barton]

The problem is to construct HoTT types whose "internal homotopy type" is the homotopy type of a real or complex Grassmannian.
Here "internal homotopy type of X" means, for example, use the interpretation of HoTT in simplicial sets and take the homotopy type of the simplicial set corresponding to X.

[Reid Barton]

Of course you can also reinvent the real numbers, classical topology, linear algebra, etc. in HoTT just the same way you would do in Lean and define Grassmannians that way, but there's no known way in book HoTT to relate this classical homotopy theory to the internal homotopy theory.

[Reid Barton]

I think there was a discussion about this here before but I can't find it now

[Kevin Buzzard]

The penny is slowly dropping. Last summer @Ali Sever developed synthetic 2-dimensional geometry in Lean (following Tarski), where "point" and "line" are just abstract types and there are relations between them. This is different to "analytic 2-dimensional geometry" where you define $\mathbb{R}^2$ and then points are points in $\mathbb{R}^2$ and lines are lines in $\mathbb{R}^2$.

This HoTT is just the same sort of thing isn't it. You're saying we can do it the "analytic" way, but this basic interpretation of types as spaces-up-to-homotopy is like the synthetic way of doing it.

[Kevin Buzzard]

This is basically explained on p4 of the thesis. "Synthetic geometry limits the things one can state or prove, but these proofs are applicable in every model of the axioms". That's all well and good, but what about if you only care about one model?

[Kevin Buzzard]

So there might be more models of HoTT other than spaces-up-to-homotopy?

[Reid Barton]

There are definitely multiple models (I know it's not in English, but see the bottom of page 2)

[Kevin Buzzard]

Hmm, yeah that doesn't really help :-/

[Kevin Buzzard]

So is "spaces up to homotopy" a "model" for HoTT?

[Kevin Buzzard]

Is "the simplicial set model" something like "simplicial sets up to some sort of simplicial homotopy relation"?

[Kevin Buzzard]

Where can I read about Grothendieck infinity,1 toposes? Assume I know what a Grothendieck topos is.

[Koundinya Vajjha]

@Kevin Buzzard this is what people usually refer to when they talk about the "simplicial set model" - https://arxiv.org/abs/1211.2851

[Reid Barton]

Where can I read about Grothendieck infinity,1 toposes? Assume I know what a Grothendieck topos is.

Instead of sheaves of sets on a site, take sheaves of spaces on a site.

[Reid Barton]

An (infinity,1)-topos is a particular kind of (infinity,1)-category, which you could model using any choice of models for (infinity,1)-categories, for example, quasicategories as in Jacob's book.

[Reid Barton]

Incidentally Lean minus all the axioms can also be interpreted in any Grothendieck topos, so this question about multiple models is sort of orthogonal to the question about HoTT or not.

[Reid Barton]

You have to do a pretty large amount of work to get from an (infinity,1)-topos to an interpretation of HoTT though

[Reid Barton]

Maybe this is the best thing to say about the spaces model:

[Kevin Buzzard]

I only know one Grothendieck topos really, and that's the category of sets :-)

[Reid Barton]

We're going to interpret a type as a simplicial set (or more accurately, a Kan complex)

[Kevin Buzzard]

Instead of sheaves of sets on a site, take sheaves of spaces on a site.

Do I have to invert homotopy equivalences though?

[Reid Barton]

and if the interpretation of T is a simplicial set $X$, then the interpretation of @eq T a b is the simplicial set of maps $\Delta^1 \to X$ sending $0$ to a and $1$ to b

[Kevin Buzzard]

Right.

[Reid Barton]

Not invert exactly but keep track of them in the higher morphisms, yes.

[Kevin Buzzard]

A simplicial version of everything.

[Kevin Buzzard]

Not invert exactly but keep track of them in the higher morphisms, yes.

Aah!

[Reid Barton]

Is that an "Aaa" or an "Ahh"

[Kevin Buzzard]

Oh I see, I am conflating two uses of "=".

[Kevin Buzzard]

I shouldn't be thinking of "X=Y" as meaning "X looks exactly the same as Y"

[Reid Barton]

Of course I should also tell you how to define the rest of the connectives but some of them are easy, for example prod becomes the product and -> becomes the mapping space (let's ignore Pi types for now)

[Kevin Buzzard]

Pi types are just some fibration or something

[Kevin Buzzard]

oh, in the simplicial world you have to make them

[Reid Barton]

So if I have f, g : X -> Y then a term t : f = g is a map $\Delta^1 \to Y^X$--which I can also treat as $X \times \Delta^1 \to Y$, i.e., a simplicial homotopy (since I assumed my spaces were Kan complexes, I can represent every homotopy which should exist this way)

[Kevin Buzzard]

How do I know that this simplicial model is definitely different to the topological spaces model?

[Reid Barton]

I think there can't really be a topological spaces model for technical reasons but if there was one it should not be different in any meaningful way

[Kevin Buzzard]

So what did you mean by "sheaves of spaces" [on a point]?

[Reid Barton]

so you can just imagine topological spaces instead of simplicial sets, if you prefer

[Reid Barton]

"Space" is a free-for-all word that means simplicial set or topological space or whatever you like that models the homotopy theory of spaces

[Kevin Buzzard]

clever!

[Reid Barton]

It's sort of analogous to how we don't care what model you pick for a $K(G,1)$ or whatever, but one level higher

[Kevin Buzzard]

So HoTT is a way of making the "basic objects" Kan complexes. And it feels to me that Lean is a way of making the basic objects into non-intersecting sets. So if you want to do some parts of homotopy theory then HoTT is a really good way to do it because the basic objects are so close to the objects you want to model. But it sounds like a less good way of doing all mathematics, because Lean's types seem to me to be closer to the kind of objects that mathematicians use. Are there people out there who would argue that I am wrong here and I should be thinking of Z/6Z or the p-adic numbers as some sort of space?

[Reid Barton]

Z/6Z no; of course you already think of the p-adic numbers as some kind of space--it's not the kind of space that HoTT helps you with, but another flavor of type theory might

[Reid Barton]

or rather than changing your type theory, you could change your model (condensed sets?)

[Kevin Buzzard]

I definitely don't think of the p-adic numbers as only being defined up to homotopy!

[Kevin Buzzard]

or rather than changing your type theory, you could change your model (condensed sets?)

Do they have anything to do with all this nonsense?

[Reid Barton]

Anyways in HoTT you can always impose a condition that makes a type X into a genuine set: namely isSet X := \Pi (a b : X) (e f : a = b), e = f

[Kevin Buzzard]

Right. And then I can perhaps prove that some things are sets.

[Kevin Buzzard]

It seems to me that I have lost the ability to rewrite, and this extra condition is some attempt to put it back again. Hmm. Maybe what I'm saying is that I have lost Prop, and one can attempt to make it again, but I bet in practice it's not as good as my beloved Lean Prop.

[Reid Barton]

and then manually use isSet where you would in Lean rely on proof irrelevance--and then you get only a propositional equality and not a definitional one. It doesn't seem very ergonomic to me, but I've never tried to use it myself.

[Reid Barton]

Basically what you just wrote

[Kevin Buzzard]

My attempt over the last couple of weeks to understand HoTT has taken some of the gloss off it. I think I'd rather have a transfer tactic than lose all this other stuff. The transfer tactic seems accessible to me.

[Reid Barton]

Now you could probably design a system with both HoTT-style types and sets, or more generally track the "h-level" of a type (= how truncated it is) the same way Lean tracks universe levels, it just doesn't exist yet as far as I know

[Kevin Buzzard]

I see. So one could imagine some future version of Leo coming along with a new model, a slightly different kind of type theory which was perhaps some way between Lean and HoTT, which worked even better for mathematics, and then we'd all have to start again?

[Reid Barton]

Or possibly we figure out how to extend/embed these systems in a way that doesn't require starting over

[Reid Barton]

The question you started with about building types in HoTT that correspond to things we classically build using geometric constructions is a big deal if you want to go far into homotopy theory, too.

[Kevin Buzzard]

It seems to me that for "normal mathematicians" (i.e. mathematicians who don't know anything about type theory or set theory or category theory), vanilla Lean 3 is currently the best option for formalising "all normal maths" on a computer. HOL has no dependent types so just isn't flexible enough for algebra (although it's very good at analysis) and HoTT is great at homotopy theory but lacks a decent implementation in a computer system. Mizar seems to be dead, for some reason, so that leaves Coq, Lean and Agda, and Lean is somehow better than the other two because it was written later on so has learnt from the mistakes of the earlier systems (quotients, term mode and tactic mode, ...)

[Kevin Buzzard]

The question you started with about building types in HoTT that correspond to things we classically build using geometric constructions is a big deal if you want to go far into homotopy theory, too.

Why? If you want to reason about complicated objects which have an analytic construction but not a synthetic one then you should figure out what extra properties you need from the analytic construction which don't "come for free" via some formal synthetic argument, right?

[Reid Barton]

Well, and then what? Add them as constants/axioms?

[Reid Barton]

If you're willing to extend the theory then you have options

[Kevin Buzzard]

Oh we're slightly at cross purposes. I was imagining building them analytically. Sure you're in trouble if you want to do everything synthetically.

[Kevin Buzzard]

sounds to me like you can't even do Grassmannians if you stick to the synthetic approach.

[Reid Barton]

Right and that means no K-theory, or complex cobordism which is at the heart of chromatic homotopy theory, etc

[Reid Barton]

So one thing I would like to attempt some day is to turn the Kapulkin-Lumsdaine paper that @Koundinya Vajjha linked earlier into Lean so that you can do the synthetic homotopy theory parts in an embedded HoTT language and the analytic parts with whatever means are necessary.

[Reid Barton]

though I have very little idea how well the "embedded HoTT language" part would work in practice

[Kevin Buzzard]

I just can't get away from the fact that HoTT is making a tool which makes some parts of homotopy theory very nice. What about the rest of maths? It's like Isabelle/HOL with its real analysis.

[Kevin Buzzard]

These tools are very suitable for parts of maths, but a lot less suitable for other parts.

[Reid Barton]

I mean, it does also solve your "if R is local and S is isomorphic to R then S is local" problem.

[Reid Barton]

I think the area where HoTT is strongest is actually category theory (and maybe n-categories for very small values of n like 2) and maybe this is why UniMath has so much of it.

[Kevin Buzzard]

I mean, it does also solve your "if R is local and S is isomorphic to R then S is local" problem.

It does, but it sounds to me like Lean might be able to make a better solution.

[Kevin Buzzard]

because Lean's solution will have computational content.

[Kevin Buzzard]

If we make some computable definition that depends on R, and then port it over to S, it should remain computable.

[Reid Barton]

Oh, I don't know whether this helps, but regarding the term "sheaf of spaces" which I never really defined, if you require the spaces to only have $\pi_0$ and $\pi_1$, then it's the same thing as a stack.

[Reid Barton]

Because a space with only $\pi_0$ and $\pi_1$ is the same thing as a groupoid

[Reid Barton]

https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/

cubicaltt is based on a novel type theory called Cubical Type Theory that provides new ways to reason about equality. Most notably it makes various extensionality principles, like function extensionality and Voevodsky’s univalence axiom, into theorems instead of axioms. This is done such that these principles have computational content and in particular that we can transport structures between equivalent types and that these transports compute. This is different from when one postulates the univalence axiom in a proof assistant like Coq or Agda. If one just adds an axiom there is no way for Coq or Agda to know how it should compute and one looses the good computational properties of type theory. In particular canonicity no longer holds and one can produce terms that are stuck (e.g. booleans that are neither true nor false but don’t reduce further). In other words this is like having a programming language in which one doesn’t know how to run the programs. So cubicaltt provides an operational semantics for Homotopy Type Theory and Univalent Foundations by giving a computational justification for the univalence axiom and (some) higher inductive types.

[Kevin Buzzard]

So how's its maths library?

[Reid Barton]

I think this is currently even more impractical to actually use though.

[Reid Barton]

For those who cannot live without implicit arguments and other features of modern proof assistants there is now an experimental cubical mode shipped with the master branch of Agda.

[Kevin Buzzard]

and presumably, like Coq or Lean, if you try it in Agda then you have to promise not to use some of Agda's functionality?

[Kevin Buzzard]

What's the easiest way of proving false using the Lean 3 HoTT package?

[Kevin Buzzard]

Is bool = fin 2 -> false provable in Lean?

[Reid Barton]

It looks like the Agda cubical thing is a mode that Agda is aware of, so it probably automatically prevents you from breaking the rules (assuming there aren't bugs), like Lean 2's HoTT mode

[Kevin Buzzard]

Maybe it's easier to write down two equivalences bool -> bool

[Kenny Lau]

Is bool = fin 2 -> false provable in Lean?

no

[Reid Barton]

What's the easiest way of proving false using the Lean 3 HoTT package?

Use univalence to construct e : bool = bool such that eq.rec on e swaps the values, and then use proof irrelevance to get e = rfl

[Kevin Buzzard]

right.

[Chris Hughes]

Is tt == ff in HoTT

[Kevin Buzzard]

Use univalence to construct e : bool = bool such that eq.rec on e swaps the values, and then use proof irrelevance to get e = rfl

dammit e has type Type 1 instead of Prop

[Kevin Buzzard]

= has been redefined to mean hott.eq

[Chris Hughes]

Are you in HoTT Lean?

[Kevin Buzzard]

rofl = is overloaded

[Kevin Buzzard]

I'm just goofing around in @Gabriel Ebner 's hott3 repo

[Kevin Buzzard]

= is overloaded! It's just like normal maths!

[Kevin Buzzard]

hott_theory_cmd "local infix ` = ` := hott.eq"

@[hott, reducible] def rfl {A : Type u} {a : A} := eq.refl a

You've got to be pretty darn careful in this repo!

[Reid Barton]

Oh I was afraid of that, but I only skimmed the source on github, I didn't actually build it.

[Kevin Buzzard]

inductive eq {A : Type u} (a : A) : A → Type u
| refl : eq a

[Reid Barton]

Okay so it's the same as the normal eq, just not a Prop.

[Kevin Buzzard]

right

[Reid Barton]

You can still prove that any two terms of type hott.eq a b are equal but it's more complicated than you might expect under the hood.

[Kevin Buzzard]

Perhaps I'm not supposed to be proving that sort of thing.

[Reid Barton]

Well that's how you finish the proof of false--it replaces the proof irrelevance step

[Reid Barton]

So yes you're not supposed to prove it

[Chris Hughes]

This always seemed to me to be something that felt accidentally consistent. You have a recursor that says every proof is refl, but somehow you can't prove everything's a set. A lot of the proofs in the HoTT book informally prove equalities by saying "assume everything's refl". Is there some intuition behind when this is valid? Very imprecise question, I know.

[Koundinya Vajjha]

So one thing I would like to attempt some day is to turn the Kapulkin-Lumsdaine paper that Koundinya Vajjha linked earlier into Lean so that you can do the synthetic homotopy theory parts in an embedded HoTT language and the analytic parts with whatever means are necessary.

AFAIK, synthetic homotopy theory uses Higher Inductive types and the Kapulkin-Lumsdaine paper avoids HITs altogether. As of last year, I think HITs have a semantics in the simplicial model, although I'm not totally sure.

[Reid Barton]

It avoids them in the sense that it does not handle them, yeah.

[Kevin Buzzard]

The definition of the $S^1$ type (the circle) seems to have one point $x$ and one proof $x=x$ and you can compose this proof with itself lots of times and get lots of proofs of $x=x$ and only one of them will be refl

[Kevin Buzzard]

This proof of $x=x$ is made as an explicit constructor in the definition of $S^1$ so is really not proved by refl

[Kevin Buzzard]

I don't even know if I'm supposed to be calling it a "proof".

[Mario Carneiro]

@Chris Hughes It's not exactly about "assume everything's refl", but it's hard not to read it that way because that's what the J rule (aka eq.drec) says

[Reid Barton]

This always seemed to me to be something that felt accidentally consistent. You have a recursor that says every proof is refl, but somehow you can't prove everything's a set. A lot of the proofs in the HoTT book informally prove equalities by saying "assume everything's refl". Is there some intuition behind when this is valid? Very imprecise question, I know.

At least one endpoint of the equality has to be a variable; then you can replace it and the equality proof by the other endpoint and refl. The intuition is that if you have a path in a space, if you're allowed to move one endpoint, then you can collapse the path down to a constant path, but if you're not allowed to then you can't. (Well that is kind of obvious, but the point is that even if the two endpoints are the same then the path might not be equal to the constant path.)

[Floris van Doorn]

Some comments:

Kevin Buzzard: So how's its [cubicaltt's] maths library?

There is none, up to a rounding error. I doubt that the rational numbers are defined. Note that cubicaltt does not support implicit arguments, and yes, that is every bit as inconvenient as you think it is.

What's the easiest way of proving false using the Lean 3 HoTT package?

The claim of consistency of the Lean 3 HoTT library is that you cannot prove false in a declaration with the @[hott] attribute without generating a warning/error message. Without this attribute you can do it, as stated above (you have to prove that hott.eq and eq are equivalent).

Is tt == ff in HoTT

If == is the heq analogue for HoTT, then yes. However, this is not in contradiction, since you cannot prove that if x == y and x : A and y : A then x = y. What this shows is that heq is not a useful notion in HoTT. Instead, we use pathovers: https://github.com/gebner/hott3/blob/master/src/hott/init/pathover.lean

= is overloaded! It's just like normal maths!

If I recall correctly, local notation doesn't overload global notation, but replaces it. But now that I test it, that doesn't seem to be true. I'm quite sure it was never a problem (presumably because hott.eq always applies when eq does [for the use cases of HoTT].

[Chris Hughes]

Is HoTT is consistent with proof irrelevance without large elimination?

[Floris van Doorn]

With "large elimination" do you mean "singleton elimination" (the reason that eq, acc, true and similar inductive propositions/predicates can eliminate to Type* instead of just Prop)? Assuming you also remove choice and quotients, then I strongly suspect it is consistent, since in that case there is probably no way to go from Prop to Type*. In other words, if you can construct an element of a type, then I suspect you can construct that element without proving any proposition.

[Chris Hughes]

This took me forever. HoTT is weird.

@[hott] example (a b : unit) : ∀ (x y : a = b), x = y :=
punit.rec_on a (λ x, @eq.rec_on _ _ (λ b h, ∀ y, eq h y) _ _ $
  λ y, @eq.rec_on unit () (λ a, punit.rec_on a (λ h, eq (eq.refl ()) h)) () y (eq.refl _))

[Kenny Lau]

are there no tactics in hott?

[Chris Hughes]

I haven't found any. cases gives the the error not hott: uses large eliminator eq.rec

[Kenny Lau]

not hott rhymes

[Chris Hughes]

Also the elaborator can never compute the motive for these funny ones.

[Gabriel Ebner]

Some tactics are available. For example, cases (and the equations compiler) works as long as the type you match on is not dependent (i.e., unit, prod, list are fine. sigma, eq is bad). Floris wrote an hinduction tactic that does induction on equalities. There is also an hsimp tactic that adapts the simplifier to work on hott.eq.

@[hott] def ex2 (a b : unit) : ∀ (x y : a = b), x = y :=
begin
intro x, hinduction x, intro y, cases a,
apply @eq.rec_on unit _ (λ ⟨⟩ h, refl _ = h) _ y,
exact rfl
end

(My HoTT is really rusty now.) BTW, @[hott] doesn't work on examples.

[Chris Hughes]

How do I prove 0 \ne nat.succ n in HoTT

[Reid Barton]

can't you do it the same way as usual?

[Kenny Lau]

spoilers: there's a proof in hott.nat.basic

[Kenny Lau]

spoilers
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
@[hott, reducible] protected def code : ℕ → ℕ → Type
| 0        0        := unit
| 0        (succ m) := empty
| (succ n) 0        := empty
| (succ n) (succ m) := code n m

@[hott] protected def refl : Πn, nat.code n n
| 0        := star
| (succ n) := refl n

@[hott] protected def encode {n m : ℕ} (p : n = m) : nat.code n m :=
p ▸ nat.refl n

@[hott] def succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
nat.encode

[Chris Hughes]

nat.no_confusion will prove it for normal eq not HoTT eq. I guess I could define nat.hno_confusion again.

[Floris van Doorn]

The nat.code/encode/decode are very similar to nat.no_confusion_type. They are a bit stronger, they also allow you to prove that n = m is equivalent (as a type) to code n m, which allows you to prove that n = m is a proposition (subsingleton), and hence that nat is a set.

[Floris van Doorn]

There are tactic proofs in HoTT3, but there are also a bunch of illegal tactics that use proof irrelevance (cases/rw/simp/...). Instead of cases you can do induction (which is less sophisticated) and Gabriel wrote HoTT-compatible versions of rw and simp called rwr and hsimp.

[Floris van Doorn]

@Chris Hughes That proof is indeed counter-intuitive. Here is the version in the HoTT library:
https://github.com/gebner/hott3/blob/64a297c4c1effa4886abcdc08dd88824a7b27455/src/hott/init/trunc.lean#L156-L161

The idea behind the proof is that you first want to define a "canonical" proof that any two elements in your type are equal (which is equal to refl when the two terms are definitionally equal), and then (using path/eq induction) proof that an arbitrary path/eq is equal to the canonical one.

You can also look in chapter 3 of the HoTT book (I think section 3.1) for a proof in words.

[Floris van Doorn]

There are plenty of tactic proofs in the HoTT library: https://github.com/gebner/hott3/search?q=begin&unscoped_q=begin

[Johan Commelin]

Here is one question that I've been wondering about:
suppose that I formalise groups in HoTT. It would be something like

class group (G : Type) :=
(set : is_a_set G)
(mul : G → G → G)
(one : G)
(axioms : blah)

The difference is of course the addition of the is_a_set condition.

Now I formalise Group as bundled groups, and endow this with the obvious category structure. I then have isomorphisms in the category Group, but HoTT also gives me transport along paths. These two notions are mathematically the same. How hard is it to derive this in HoTT?

[Reid Barton]

I'm pretty sure the chapter on categories in the hott book discusses this exact issue

[Reid Barton]

This condition that the groupoid of isomorphisms agrees with the homotopy type of the space of objects is something you can write down internally

[Reid Barton]

For Set it is the univalence axiom (for sets)

[Reid Barton]

I forget what the hott book calls it, but it's essentially the "complete" condition of complete Segal spaces

[Reid Barton]

I'm pretty sure the book explains why it is also automatically satisfied for algebraic structures like groups

[Johan Commelin]

Ok, thanks. I should have a look at the HoTT book again.
With "automatically satisfied" you mean that it is true, not that you get the result for free, I guess.

[Reid Barton]

right

[Reid Barton]

but I don't think it should be very hard, and it should be mechanical

[Scott Morrison]

You know that the cool kids these days define a group as a tuple:
(G : Type) (BG : Type) (h : G = \Omega BG) ...

[Scott Morrison]

(i.e. it's some type which is the loop space of some other type)

[Julian Berman]

Hi. I have a few layman's Lean history or mathematics questions after reading the README of Gabriel's HoTT repo (my goal is just to make sure I know enough to competently write something in this PR, but I'd love to understand more than I do now regardless):

the equality type eq which is defined to be in Prop can eliminate to Type, which is inconsistent with univalence

• Is there an easy way to understand what makes this inconsistent with univalence?
• What was the historical reason to introduce this change (singleton elimination) to Lean 3?
• Is this the only thing inconsistent with univalence? It seems the answer is "yes", given that the external repo was able to re-add a HoTT-based library with just some avoidance of that, but just want to make sure I didn't miss something
• What is a higher inductive type? Is it equiimportant with the univalence axiom in understanding HoTT and how it differs from Lean / CoC?
• Can a layman understand "Dan Licata's trick"? What's the "problem" that needs a trick?

And finally:

Without singleton elimination the system is conjectured to be consistent

Is this still the best that can be said there?

[Kevin Buzzard]

My two cents: if X and Y are types with two terms like bool then we can construct two provably distinct terms f g : X ≃ Y but there's at most one term h : X = Y in lean because X = Y is a Prop. So X ≃ Y and X = Y provably don't biject with each other.

My personal understanding of why Leo dropped univalence was that he basically felt that it made the system complex and unintuitive to use and maintain.

[Chris Hughes]

Julian Berman said:

• Is this the only thing inconsistent with univalence? It seems the answer is "yes", given that the external repo was able to re-add a HoTT-based library with just some avoidance of that, but just want to make sure I didn't miss something

The axiom of choice is the other big thing that's inconsistent with univalence depending on how it's stated. Lean's statement would be inconsistent but wrapping it in nonempty would make it consistent, so you can have Pi {A : Type}, nonempty (nonempty A -> A)

[Chris Hughes]

Julian Berman said:

• What is a higher inductive type? Is it equiimportant with the univalence axiom in understanding HoTT and how it differs from Lean / CoC?

A higher inductive type is like an inductive type but you can also add paths (equalities) between elements in your type. This is one way of doing quotient types, but it also lets you define things like the space S^1which is defined as follows.

data S¹ : Type₀ where
  base : S¹
  loop : base ≡ base

You can add an extra path between base and base which is not equal to refl. The space of paths base ≡ base can be proved to be isomorphic to int and you can do this in the HoTT game.

[Patrick Massot]

It looks like those people forget to write where they got their inspiration.

[Patrick Massot]

The very first commit in July 2021 contained a text file explicitly referring to the Natural Number Game, but somehow that information got lost...

[Reid Barton]

Chris Hughes said:

Julian Berman said:

• What is a higher inductive type? Is it equiimportant with the univalence axiom in understanding HoTT and how it differs from Lean / CoC?

A higher inductive type is like an inductive type but you can also add paths (equalities) between elements in your type.

And "Dan Licata's trick" is a way to simulate HITs in a system that was not designed to support them.
The idea is to represent a HIT by an ordinary inductive that only has the value constructors (like base but not loop). Then add the path constructors as axioms. This usually makes the system inconsistent, because we could prove (using the original induction principle for the underlying inductive type) that these axioms are false. So, we do this inside a private scope from which we don't export the original induction principle, but instead export our own induction principle with the correct type for the HIT (with an extra argument corresponding to the path constructor).

[Reid Barton]

Kevin Buzzard said:

My personal understanding of why Leo dropped univalence was that he basically felt that it made the system complex and unintuitive to use and maintain.

It seems to be very hard to support multiple foundational systems well at the same time. The issue is not so much in the kernel/prover itself but in the surrounding libraries--if the systems are different in useful ways then you will want to express things differently in them, and then the libraries diverge. In the case of two mutually incompatible systems (e.g. univalence vs large elimination for eq/choice constant) you actually have three systems, the third being the "neutral" system containing whatever is valid in both of them.

We already have something similar regarding decidability--parts of the library that are totally nonconstructive still have to deal with decidable and fintype instances and potential diamonds and stating lemmas "correctly" and so on.

[Reid Barton]

Julian Berman said:

• What was the historical reason to introduce this change (singleton elimination) to Lean 3?

This is a slight simplification but: In practice, the choice is between having definitional proof irrelevance for x = y and having univalence for = between types. You can't have both because there are generally multiple distinct equivalences between two types.
Definitional proof irrelevance for x = y is nice because it means that you can be reasonably confident that changing the proof of an equality won't break downstream proofs, and so you can freely use tactics/automation without worrying that a change to the tactic will make it produce the "wrong" proof.

[Joseph Hua]

Patrick Massot said:

It looks like those people forget to write where they got their inspiration.

Thanks for pointing this out. I added some info on the website https://thehottgameguide.readthedocs.io/en/latest/getting-started/about-hott-game.html

[Gabriel Ebner]

My personal understanding of why Leo dropped univalence was that he basically felt that it made the system complex and unintuitive to use and maintain.

If I recall correctly, the immediate reason for dropping HoTT was that it was incompatible with the code extraction for the VM. In HoTT, an argument h : x = y cannot be dropped because it can be executed (h.elim might e.g. be Boolean negation). However we want to erase proofs for performance reasons.

[Kevin Buzzard]

My comments are a muddled recollection of something Leo told me verbally once, of the form "it was hard to make it work efficiently". Probably Gabriel's comments are a more precise summary of the story