# Zulip Chat Archive

## Stream: maths

### Topic: HoTT

#### Kevin Buzzard (May 25 2019 at 10:17):

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 (May 25 2019 at 10:25):

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 (May 25 2019 at 10:27):

`trunc`

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

#### Reid Barton (May 25 2019 at 10:35):

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 (May 25 2019 at 10:41):

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

#### Reid Barton (May 25 2019 at 10:52):

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 (May 25 2019 at 11:01):

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

#### Reid Barton (May 25 2019 at 11:01):

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

#### Reid Barton (May 25 2019 at 11:03):

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

#### Mario Carneiro (May 25 2019 at 11:10):

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

#### Mario Carneiro (May 25 2019 at 11:11):

I think it slowed down when Voevodsky died though

#### Kevin Buzzard (May 25 2019 at 11:11):

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 (May 25 2019 at 11:11):

So unimath is to mathlib as hott is to lean?

#### Mario Carneiro (May 25 2019 at 11:12):

I think so, I'm no expert though

#### Kevin Buzzard (May 25 2019 at 11:13):

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

#### Mario Carneiro (May 25 2019 at 11:14):

I certainly wouldn't be able to answer that

#### Mario Carneiro (May 25 2019 at 11:14):

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

#### Kevin Buzzard (May 25 2019 at 11:14):

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

#### Mario Carneiro (May 25 2019 at 11:15):

I guess the UniMath foundation?

#### Kevin Buzzard (May 25 2019 at 11:15):

Hopefully someone will respond to my post on the mailing list

#### Kevin Buzzard (May 25 2019 at 11:15):

Thanks, I'll try them

#### Mario Carneiro (May 25 2019 at 11:16):

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 (May 25 2019 at 11:16):

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

#### Mario Carneiro (May 25 2019 at 11:17):

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 (May 25 2019 at 11:18):

Does unimath work only with constructive maths??

#### Kevin Buzzard (May 25 2019 at 11:18):

No such system will ever catch on with mathematicians

#### Mario Carneiro (May 25 2019 at 11:19):

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 (May 25 2019 at 11:19):

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 (May 25 2019 at 11:20):

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

#### Mario Carneiro (May 25 2019 at 11:21):

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

#### Kevin Buzzard (May 25 2019 at 11:22):

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

#### Mario Carneiro (May 25 2019 at 11:22):

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

#### Reid Barton (May 25 2019 at 11:27):

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 (May 25 2019 at 12:15):

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 (May 25 2019 at 12:22):

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

#### Chris Hughes (May 25 2019 at 12:28):

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 (May 25 2019 at 12:29):

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 (May 25 2019 at 12:30):

What's the difference between `nonempty`

and `trunc`

in HoTT?

#### Reid Barton (May 25 2019 at 12:31):

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

#### Chris Hughes (May 25 2019 at 12:31):

So unique choice is `id`

?

#### Reid Barton (May 25 2019 at 12:31):

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

in HoTT

#### Reid Barton (May 25 2019 at 12:32):

or let's say `|| Σ ... ||`

to be more clear

#### Reid Barton (May 25 2019 at 12:33):

where `|| ... ||`

is the propositional truncation (Lean `trunc`

)

#### Reid Barton (May 25 2019 at 12:34):

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 (May 25 2019 at 12:35):

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 (May 25 2019 at 12:35):

But it's a theorem

#### Kevin Buzzard (May 25 2019 at 12:53):

Is UniMath written in book HoTT?

#### Reid Barton (May 25 2019 at 13:08):

"Close enough"

#### Reid Barton (May 25 2019 at 13:09):

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

#### Kevin Buzzard (May 25 2019 at 13:11):

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 (May 25 2019 at 13:12):

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 (May 25 2019 at 13:36):

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 (May 25 2019 at 13:38):

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

#### Koundinya Vajjha (May 25 2019 at 13:45):

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 (May 25 2019 at 13:46):

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

#### Kevin Buzzard (May 25 2019 at 13:48):

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 (May 25 2019 at 13:55):

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 (May 25 2019 at 14:24):

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

#### Mario Carneiro (May 25 2019 at 14:25):

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 (May 25 2019 at 14:25):

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

#### Mario Carneiro (May 25 2019 at 14:27):

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 (May 25 2019 at 14:39):

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 (May 27 2019 at 17:07):

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 (May 27 2019 at 17:14):

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 (May 27 2019 at 17:20):

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 (May 27 2019 at 21:28):

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

#### Floris van Doorn (May 27 2019 at 21:52):

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 (May 27 2019 at 23:02):

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

#### Kevin Buzzard (Jun 02 2019 at 17:59):

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 (Jun 04 2019 at 09:34):

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

#### Kevin Buzzard (Jun 04 2019 at 12:12):

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

#### Rob Lewis (Jun 04 2019 at 12:24):

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 (Jun 08 2019 at 22:06):

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 (Jun 08 2019 at 22:15):

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 (Jun 08 2019 at 22:24):

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 (Jun 08 2019 at 22:26):

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

#### Kevin Buzzard (Jun 08 2019 at 22:28):

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 (Jun 08 2019 at 22:29):

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 (Jun 08 2019 at 22:30):

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

#### Reid Barton (Jun 08 2019 at 22:30):

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

#### Kevin Buzzard (Jun 08 2019 at 22:31):

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

#### Kevin Buzzard (Jun 08 2019 at 22:32):

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

#### Kevin Buzzard (Jun 08 2019 at 22:33):

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

#### Kevin Buzzard (Jun 08 2019 at 22:33):

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

#### Koundinya Vajjha (Jun 08 2019 at 22:38):

@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 (Jun 08 2019 at 22:55):

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 (Jun 08 2019 at 22:56):

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 (Jun 08 2019 at 22:58):

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 (Jun 08 2019 at 22:59):

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 (Jun 08 2019 at 23:00):

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

#### Kevin Buzzard (Jun 08 2019 at 23:00):

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

#### Reid Barton (Jun 08 2019 at 23:00):

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

#### Kevin Buzzard (Jun 08 2019 at 23:01):

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 (Jun 08 2019 at 23:02):

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 (Jun 08 2019 at 23:02):

Right.

#### Reid Barton (Jun 08 2019 at 23:02):

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

#### Kevin Buzzard (Jun 08 2019 at 23:03):

A simplicial version of everything.

#### Kevin Buzzard (Jun 08 2019 at 23:03):

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

Aah!

#### Reid Barton (Jun 08 2019 at 23:03):

Is that an "Aaa" or an "Ahh"

#### Kevin Buzzard (Jun 08 2019 at 23:03):

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

#### Kevin Buzzard (Jun 08 2019 at 23:04):

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

#### Reid Barton (Jun 08 2019 at 23:04):

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 (Jun 08 2019 at 23:05):

Pi types are just some fibration or something

#### Kevin Buzzard (Jun 08 2019 at 23:05):

oh, in the simplicial world you have to make them

#### Reid Barton (Jun 08 2019 at 23:05):

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 (Jun 08 2019 at 23:06):

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

#### Reid Barton (Jun 08 2019 at 23:07):

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 (Jun 08 2019 at 23:08):

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

#### Reid Barton (Jun 08 2019 at 23:08):

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

#### Reid Barton (Jun 08 2019 at 23:08):

"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 (Jun 08 2019 at 23:08):

clever!

#### Reid Barton (Jun 08 2019 at 23:10):

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 (Jun 08 2019 at 23:11):

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 (Jun 08 2019 at 23:13):

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 (Jun 08 2019 at 23:13):

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

#### Kevin Buzzard (Jun 08 2019 at 23:14):

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

#### Kevin Buzzard (Jun 08 2019 at 23:14):

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 (Jun 08 2019 at 23:14):

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 (Jun 08 2019 at 23:15):

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

#### Kevin Buzzard (Jun 08 2019 at 23:16):

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 (Jun 08 2019 at 23:16):

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 (Jun 08 2019 at 23:16):

Basically what you just wrote

#### Kevin Buzzard (Jun 08 2019 at 23:17):

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 (Jun 08 2019 at 23:18):

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 (Jun 08 2019 at 23:19):

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 (Jun 08 2019 at 23:24):

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

#### Reid Barton (Jun 08 2019 at 23:29):

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 (Jun 08 2019 at 23:29):

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 (Jun 08 2019 at 23:30):

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 (Jun 08 2019 at 23:31):

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

#### Reid Barton (Jun 08 2019 at 23:31):

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

#### Kevin Buzzard (Jun 08 2019 at 23:32):

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 (Jun 08 2019 at 23:32):

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

#### Reid Barton (Jun 08 2019 at 23:32):

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

#### Reid Barton (Jun 08 2019 at 23:33):

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 (Jun 08 2019 at 23:34):

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

#### Kevin Buzzard (Jun 08 2019 at 23:36):

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 (Jun 08 2019 at 23:36):

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

#### Reid Barton (Jun 08 2019 at 23:37):

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

#### Reid Barton (Jun 08 2019 at 23:38):

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 (Jun 08 2019 at 23:42):

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 (Jun 08 2019 at 23:43):

because Lean's solution will have computational content.

#### Kevin Buzzard (Jun 08 2019 at 23:43):

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

#### Reid Barton (Jun 08 2019 at 23:49):

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 (Jun 08 2019 at 23:49):

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

#### Reid Barton (Jun 08 2019 at 23:56):

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 (Jun 08 2019 at 23:57):

So how's its maths library?

#### Reid Barton (Jun 08 2019 at 23:57):

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

#### Reid Barton (Jun 08 2019 at 23:57):

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 (Jun 08 2019 at 23:58):

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 (Jun 08 2019 at 23:59):

What's the easiest way of proving `false`

using the Lean 3 HoTT package?

#### Kevin Buzzard (Jun 09 2019 at 00:00):

Is `bool = fin 2 -> false`

provable in Lean?

#### Reid Barton (Jun 09 2019 at 00:02):

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 (Jun 09 2019 at 00:02):

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

#### Kenny Lau (Jun 09 2019 at 00:02):

Is

`bool = fin 2 -> false`

provable in Lean?

no

#### Reid Barton (Jun 09 2019 at 00:04):

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 (Jun 09 2019 at 00:05):

right.

#### Chris Hughes (Jun 09 2019 at 00:05):

Is `tt == ff`

in HoTT

#### Kevin Buzzard (Jun 09 2019 at 00:07):

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 (Jun 09 2019 at 00:07):

`=`

has been redefined to mean `hott.eq`

#### Chris Hughes (Jun 09 2019 at 00:08):

Are you in HoTT Lean?

#### Kevin Buzzard (Jun 09 2019 at 00:08):

rofl `=`

is overloaded

#### Kevin Buzzard (Jun 09 2019 at 00:08):

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

#### Kevin Buzzard (Jun 09 2019 at 00:08):

`=`

is overloaded! It's just like normal maths!

#### Kevin Buzzard (Jun 09 2019 at 00:10):

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 (Jun 09 2019 at 00:10):

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

#### Kevin Buzzard (Jun 09 2019 at 00:11):

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

#### Reid Barton (Jun 09 2019 at 00:11):

Okay so it's the same as the normal `eq`

, just not a Prop.

#### Kevin Buzzard (Jun 09 2019 at 00:11):

right

#### Reid Barton (Jun 09 2019 at 00:15):

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 (Jun 09 2019 at 00:16):

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

#### Reid Barton (Jun 09 2019 at 00:17):

Well that's how you finish the proof of `false`

--it replaces the proof irrelevance step

#### Reid Barton (Jun 09 2019 at 00:17):

So yes you're not supposed to prove it

#### Chris Hughes (Jun 09 2019 at 00:25):

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 (Jun 09 2019 at 00:25):

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 (Jun 09 2019 at 00:26):

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

#### Kevin Buzzard (Jun 09 2019 at 00:26):

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 (Jun 09 2019 at 00:27):

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 (Jun 09 2019 at 00:27):

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

#### Mario Carneiro (Jun 09 2019 at 00:34):

@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 (Jun 09 2019 at 00:35):

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 (Jun 09 2019 at 10:41):

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 (Jun 09 2019 at 12:31):

Is HoTT is consistent with proof irrelevance without large elimination?

#### Floris van Doorn (Jun 10 2019 at 02:35):

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 (Jun 11 2019 at 11:51):

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 (Jun 11 2019 at 11:53):

are there no tactics in hott?

#### Chris Hughes (Jun 11 2019 at 11:54):

I haven't found any. `cases`

gives the the error `not hott: uses large eliminator eq.rec`

#### Kenny Lau (Jun 11 2019 at 11:54):

`not hott`

rhymes

#### Chris Hughes (Jun 11 2019 at 11:55):

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

#### Gabriel Ebner (Jun 11 2019 at 12:39):

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 (Jun 11 2019 at 12:55):

How do I prove `0 \ne nat.succ n`

in HoTT

#### Reid Barton (Jun 11 2019 at 12:57):

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

#### Kenny Lau (Jun 11 2019 at 12:59):

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

#### Kenny Lau (Jun 11 2019 at 13:02):

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 (Jun 11 2019 at 13:02):

`nat.no_confusion`

will prove it for normal `eq`

not HoTT `eq`

. I guess I could define `nat.hno_confusion`

again.

#### Floris van Doorn (Jun 12 2019 at 01:58):

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 (Jun 12 2019 at 01:59):

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 (Jun 12 2019 at 02:05):

@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 (Jun 12 2019 at 02:07):

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

#### Johan Commelin (Jun 12 2019 at 15:50):

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 (Jun 12 2019 at 16:00):

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

#### Reid Barton (Jun 12 2019 at 16:03):

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 (Jun 12 2019 at 16:04):

For Set it is the univalence axiom (for sets)

#### Reid Barton (Jun 12 2019 at 16:05):

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

#### Reid Barton (Jun 12 2019 at 16:06):

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

#### Johan Commelin (Jun 12 2019 at 16:48):

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 (Jun 12 2019 at 16:56):

right

#### Reid Barton (Jun 12 2019 at 16:56):

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

#### Scott Morrison (Jun 12 2019 at 21:55):

You know that the cool kids these days define a group as a tuple:

`(G : Type) (BG : Type) (h : G = \Omega BG)`

...

#### Scott Morrison (Jun 12 2019 at 21:55):

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

Last updated: May 09 2021 at 11:09 UTC