what is wrong with HoTT

Stream: general

[Johan Commelin]

Let me start by saying that I really don't want to start a flamewar. I am just very uneducated.
My question is simply this:
Is there a documented reason why mathlib chose "classical DTT" instead of HoTT + univalence?
Has there been some experience that shows that HoTT makes daily life for the working formalising mathematician harder rather than easier?

Motivation: in the https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/tutorial thread there is a discussion going on about transport of structure. And this is not the first time this has happened. If I understand univalence correctly, one would just be able to apply univalence to the equiv, which turns it into an identity. By induction on identity, one would be reduced to proving a claim that is rfl. Maybe I'm drastically oversimplifying. Maybe I misunderstand univalence. But this truly sounds like what mathematicians do "between the lines".
Please educate me.

[Andrew Ashworth]

I'm also curious about HoTT. So I think from the thread people were discussing

lemma card_eq_of_equiv {s : finset α} {t : finset β} (h : s.to_set ≃ t.to_set) :s.card = t.card :=  sorry

AFAIK the univalence axiom is (X=Y)→(X≃Y). How do you apply it in this case? Wouldn't you need (X≃Y)→(X=Y)?

[Reid Barton]

The function (X=Y)→(X≃Y) comes for free. Univalence says that it is an equivalence.

[Chris Hughes]

(X=Y)→(X≃Y) doesn't look like it needs any extra axioms. I think univalence is (X≃Y)→(X=Y). I'm curious about how it works with isomorphisms of structures, If I have two isomorphic rings R and S, do I know (1 : R) == (1 : S). Equality of the types doesn't seem like a very strong axiom.

[Chris Hughes]

In fact (1 : R) == (1 : S) seems like it could lead to some easy contradictions, but do I know anything a bit like that?

[Kevin Buzzard]

If you're using the correct equiv (ring isomorphisms) you know that the function maps one to the other of course

[Chris Hughes]

What does univalence actually say?

[Kevin Buzzard]

No idea, I'd love to know more about HOTT. Can it do perfectoid spaces?

[Bryan Gin-ge Chen]

There's this recent talk from the Voevodsky memorial conference by Benedikt Ahrens titled "Univalent foundations and the equivalence principle". I haven't watched it yet though.

[Andrew Ashworth]

How does univalence save you work? You'd still have to prove the isomorphism you chose to encode in equiv preserves structure

[Chris Hughes]

I tried googling it, and it seems like it doesn't assume proof irrelevance. It's stated as something like (A = B) ≃ (A ≃ B), where ≃ means the same thing as it does in Lean.

[Reid Barton]

IIRC "book HoTT" has no built-in Prop/Type distinction, so no proof irrelevance in that sense

[Reid Barton]

If you see Prop in a book HoTT context, it means basically the same as what we call a subsingleton

[Johan Commelin]

There's this recent talk from the Voevodsky memorial conference by Benedikt Ahrens titled "Univalent foundations and the equivalence principle". I haven't watched it yet though.

Thanks for this link. I think from 49.30 onwards it might be pretty relevant to this thread.

[Johan Commelin]

How does univalence save you work? You'd still have to prove the isomorphism you chose to encode in equiv preserves structure

Right. But in the case of Bryan's problem, there is not structure. So we win.

[Johan Commelin]

In the case of Chris's example, he is talking about (1 : R), so you need an equiv (or path, in HoTT-speak) that preserves has_one.

[Johan Commelin]

@Mario Carneiro Can you shed some light on these questions?

Is there a documented reason why mathlib chose "classical DTT" instead of HoTT + univalence?
Has there been some experience that shows that HoTT makes daily life for the working formalising mathematician harder rather than easier?

[Chris Hughes]

I guess implementing it in Lean involve creating a non proof irrelevant version of eq and implementing it using that?

[Kevin Buzzard]

Is that exactly the equiv?

[Kevin Buzzard]

Oh you mean there are parts of the eq API which need to be ported to equiv?

[Reid Barton]

You need the recursor, because the point is to be able to show things like "if R is artinian and S is isomorphic to R, then S is artinian" by applying univalence and then doing cases on the equality you get out so that you can assume S is R

[Chris Hughes]

I've thought about it some more, and I think what it would actually look like is eq,rec_on with equiv instead of eq

[Kevin Buzzard]

eq.rec_on : Π {α : Sort u_3} {a : α} {C : α → Sort u_2} {a_1 : α}, a = a_1 → C a → C a_1

[Kevin Buzzard]

So the idea would be that there would be some typeclass [plays_well_with_equiv C]?

[Reid Barton]

But I don't think you can really go about it this way, unless you can rule out "being equal to R" as a property which you can apply the recursor to.

[Reid Barton]

Because then you could just conclude that S = R.

[Kevin Buzzard]

that rule doesn't get tagged with my cool typeclass though

[Reid Barton]

Right, so plays_well_with_equiv seems to be viable and I think it's what people were calling "transportable" earlier

[Chris Hughes]

Another way might be equiv A B -> for all C : Sort u -> Sort v, C A = C B

[Kevin Buzzard]

plus the typeclass on C

[Kevin Buzzard]

Oh wait -- you want C A = C B? Not just an equiv?

[Andrew Ashworth]

ah, this paper points out a big problem with hott https://hal.inria.fr/hal-01559073v2/document. Just like with acc, you get stuck terms when you use axiomatic univalence

[Kevin Buzzard]

But does that stop me from defining a perfectoid space?

[Patrick Massot]

Why are we having this discussion again? I thought HoTT is irremediably tied to constructive mathematics.

[Andrew Ashworth]

if restriction maps, id, and def reduction made you tear your hair out, trying to deal with univalence will do so similarly

[Mario Carneiro]

Motivation: in the https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/tutorial thread there is a discussion going on about transport of structure. And this is not the first time this has happened. If I understand univalence correctly, one would just be able to apply univalence to the equiv, which turns it into an identity. By induction on identity, one would be reduced to proving a claim that is rfl.

I had a discussion with @Jeremy Avigad on this very issue today. What you have said is not wrong; you can use univalence to prove these kinds of theorems almost trivially, because it's basically the content of that axiom. But there are some huge asterisks that come with this assertion, which make it almost disingenuous to trot out as an advantage of HoTT, because even if in an alternate universe mathlib was based on HoTT we would still have a considerable amount of difficulty with transfer of structure proofs in exactly the form we want them to be, the problem would just be with different parts of the proof

[Mario Carneiro]

(X=Y)→(X≃Y) doesn't look like it needs any extra axioms. I think univalence is (X≃Y)→(X=Y). I'm curious about how it works with isomorphisms of structures, If I have two isomorphic rings R and S, do I know (1 : R) == (1 : S). Equality of the types doesn't seem like a very strong axiom.

HoTT is kind of magic when it comes to this. One of the things which is the most impressive about how HoTT works is how it always seems to get exactly the right kind of equivalence between objects. Two types are equal iff they are (constructively) bijective, two bundled groups are equal iff they are isomorphic as groups, two bundled rings are equal iff they are isomorphic as rings.

[Mario Carneiro]

In HoTT, == is actually a "bad" notion of equality. Instead they have a "pathover" a =[h] b where h : A = B, which is basically equivalent to cast a h = b

[Mario Carneiro]

The key is that equality of sigma types \Sigma x : A, B x = \Sigma x : A', B' x is the same as the pair of an equality h : A = A' and a pathover B x =[h] B' x. For a simple example, consider equality of pointed types (i.e. a type with a zero element and no axioms). This can be defined as \Sigma A : Type, A, and so an equality of sigma types (A, a) and (A', a') is an equality h : A = A' with a pathover a =[h] a'. If you unpack this, it means h is a bijective function from A to A' such that h maps a to a'. In other words, it is a pointed equivalence, which is what we wanted

[Mario Carneiro]

If you do this with groups, the pathover thing exactly asserts that the map between types preserves the 0, inv, + which is a group isomorphism

[Mario Carneiro]

How does univalence save you work? You'd still have to prove the isomorphism you chose to encode in equiv preserves structure

In HoTT, the equiv is just a plain equiv, i.e. a function f with an inverse g and two paths f o g = id, g o f = id. That is, it looks just like the usual definition of equiv, but the new interpretation gives it magic powers to be a group isomorphism when talking about groups, etc.

[Mario Carneiro]

I tried googling it, and it seems like it doesn't assume proof irrelevance. It's stated as something like (A = B) ≃ (A ≃ B), where ≃ means the same thing as it does in Lean.

Technically, it's not just any equiv, it asserts that the natural map A = B -> A ≃ B is an equivalence

[Mario Carneiro]

HoTT is inconsistent with proof irrelevance

[Mario Carneiro]

because if equalities of groups are group isos, we can't possibly assert there is only one

[Mario Carneiro]

I guess implementing it in Lean involve creating a non proof irrelevant version of eq and implementing it using that?

Yes, but it's not that simple. Just the fact that propositional equality exists in the system is enough to prove that Type eq and Prop eq are equivalent, and hence the fact that Prop eq is proof irrelevant collapses Type eq. In the hott3 library they go to great lengths to mark everything using Prop eq as "bad" and unusable in HoTT stuff to avoid contradictions

[Mario Carneiro]

I've thought about it some more, and I think what it would actually look like is eq,rec_on with equiv instead of eq

Yes, this is an equivalent way to state univalence. Something with the same recursor as eq is provably equivalent to eq, and vice versa

[Mario Carneiro]

Another way might be equiv A B -> for all C : Sort u -> Sort v, C A = C B

Oh wait -- you want C A = C B? Not just an equiv?

These are equivalent. Even if you only had A ≃ B -> for all C : Sort u -> Sort v, C A ≃ C B you could just apply it to C = \lam x, A = x to deduce (A = A) ≃ (A = B), and since the first is inhabited you just apply the function to prove A = B. So this is also univalence

[Mario Carneiro]

ah, this paper points out a big problem with hott https://hal.inria.fr/hal-01559073v2/document . Just like with acc, you get stuck terms when you use axiomatic univalence

This is why cubical type theory was invented. It provides a way to compute with univalence

[Scott Morrison]

"provides a way to compute with univalence" maybe should be "hopefully provides a way to compute with univalence, except that currently some of the things we think should compute instead blow up our computers".

[Scott Morrison]

(If I understood the cubical type theorists at Dagstuhl talking about Brunerie's number correctly.)

[Chris Hughes]

I watched the talk and the main thing I don't understand is why and when Id is not a subsingleton. If i define it in a similar in Lean, as Type, so without proof irrelevance, but it's still a subsingleton.

inductive Id {α : Type} (x : α) : α → Type
| refl : Id x

instance {α : Type} (x y : α) : subsingleton (Id x y) :=
⟨λ i j, begin cases i, cases j, refl end⟩

example {α : Type} (x y : α) (i j : Id x y) : Id i j :=
by cases i; cases j; exact Id.refl _

The recursors/ eliminators/ computation rules mentioned in the talk https://www.youtube.com/watch?v=okx4Uklvwco are the same as they are in Lean, so why do they not imply Id is a subsingleton? Obviously there are types where it is a subsingleton, which he calls "Sets", what would make a type a Set?

[Reid Barton]

Something subtle is happening in your examples. Check out what the equation compiler actually generated.

[Reid Barton]

If you try to implement these by hand, you can do the case analysis on i but then you'll get stuck on j.

[Mario Carneiro]

Reid is right. cases and the equation compiler use a HoTT-unsound proof method that introduces Prop eq to eliminate from inductive predicates. In the end the resulting proof uses the assumption that a proof of a = a is definitionally refl, which is provably false in HoTT

[Johan Commelin]

Why are we having this discussion again? I thought HoTT is irremediably tied to constructive mathematics.

@Patrick Massot The last sentence of §7 in https://arxiv.org/pdf/1711.01477.pdf (by Dan Grayson) says: "The Law of Excluded Middle and the Axiom of Choice are also validated by this interpretation, so classical mathematics is supported soundly by the univalent foundations."
So I wonder if you (we?) have been tricked by a version of the myth that all formalised math needs to be constructive.
Or is Dan Grayson pulling a trick on us?

[Mario Carneiro]

The excluded middle and the axiom of choice are indeed consistent with HoTT

[Mario Carneiro]

choice is not

[Mario Carneiro]

"The axiom of choice" here means classical.axiom_of_choice, that is, the one that ends in an existential

[Mario Carneiro]

But actually that's kind of a lie, because in HoTT you have an explicit "propositional truncation" operator that has the same role as putting things in Prop in lean

[Mario Carneiro]

there is no proof irrelevant universe in HoTT, like I said that's not consistent

[Mario Carneiro]

I think it would be instructional to actually look at Dan Grayson's work in UniMath and judge for yourself whether the style of mathematics being done there works for you. They also are aiming for the formalization of conventional mathematics, although HoTT-isms are a frequent distraction (e.g. "ooh, I wonder if transfinite induction still holds over n-types")

[Mario Carneiro]

just as constructive math is an occasional distraction here

[Scott Olson]

To respond to the original question, it's my understanding that Lean/mathlib is using more traditional type theory rather than HoTT basically "by default". Research is on-going wrt formalizing mathematics with HoTT and making univalence compute via things like cubical types but it's still a bit avant-garde

[Mario Carneiro]

I think that's fair. I would even possibly go so far as to say that we tried it and it "didn't work" in the sense that the issues thrown up are not minor annoyances but major research projects

[Johan Commelin]

there is no proof irrelevant universe in HoTT, like I said that's not consistent

But if you have a P : Prop and x y : P, then you would know that Id p q is contractible. Which seems to me just as good as proof irrelevance. In practice, I think you can even teach the computer to use this fact, without bothering you with it.

[Mario Carneiro]

I don't think HoTT is really suitable as a practical foundation for all of math, except in the logical sense

[Mario Carneiro]

But if you have a P : Prop and x y : P, then you would know that Id p q is contractible.

This is not true

[Mario Carneiro]

this is the same as chris's proof attempt, and it's not provable

[Johan Commelin]

I think that's fair. I would even possibly go so far as to say that we tried it and it "didn't work" in the sense that the issues thrown up are not minor annoyances but major research projects

This is exactly what I would like to know about. Are those problems even there if you don't care about computability?

[Mario Carneiro]

It's provably false with HITs, or even just with type equalities using univalence

[Johan Commelin]

But if you have a P : Prop and x y : P, then you would know that Id p q is contractible.

This is not true

I thought it was the definition of being a Prop in HoTT.

[Mario Carneiro]

For example, S^1 is a higher inductive type defined by base : S^1 and loop : base = base. Since this is a "free" construction, this base is not refl base

[Mario Carneiro]

Oh, I missed that you said it was a prop

[Johan Commelin]

Sure, that makes all the difference.

[Mario Carneiro]

That's not how it works in HoTT. Instead you would say P : Type and is_prop P

[Scott Olson]

props are defined as types whose path space is contractible

[Mario Carneiro]

and is_prop is basically subsingleton

[Mario Carneiro]

because there is no "universe of props"

[Johan Commelin]

Anyway, does this mean that proof irrelevance is there in the cases that we actually care about? (The other things just aren't proofs. They are higher order.)

[Mario Carneiro]

No. Being a proposition is a property which may or may not hold, and it holds a lot less than you would expect

[Johan Commelin]

def Prop := subtype is_prop wouldn't cut it, I guess.

[Mario Carneiro]

There is trunc though (indeed I borrowed the terminology from HoTT), which will make a subsingleton from any type

[Johan Commelin]

No. Being a proposition is a property which may or may not hold, and it holds a lot less than you would expect

(Emphasis mine). This is important information! Has this been documented somewhere?

[Mario Carneiro]

and things like exists and or are defined by truncating after taking the sum/sigma

[Mario Carneiro]

But I think that equalities not being subsingletons will get in your way a lot more than you think

[Mario Carneiro]

Here is a question: How do you define a group in HoTT?

[Johan Commelin]

I mean... what I'm getting from this thread is that there are "problems" with HoTT in practice. And I already had this vague feeling. But otoh, univalence seems a mathematician's dream. So I would like to understand those "problems" in more detail. And I'm asking whether someone wrote some docs saying: here's some problems for the working mathematician (someone who doesn't care about constructivity and computability, a priori).
Does something like this exist?

[Johan Commelin]

Here is a question: How do you define a group in HoTT?

Benedikt did this for monoids in that talk.

[Johan Commelin]

So it is (M : Set, mul : M × M → M, e : M, 3 proofs)

[Johan Commelin]

And I'm using his notation.

[Johan Commelin]

But Set should probably be Type + is_set M

[Mario Carneiro]

I am alluding to the Set part

[Mario Carneiro]

I guarantee you that will be a sticking point for getting mathematicians involved

[Johan Commelin]

Ok, what's wrong with it?

[Mario Carneiro]

It is a restriction that people don't want to have to think about

[Mario Carneiro]

There is an obvious definition of a group where you say Type instead, and it's not correct, and it will take you a while to realize this

[Johan Commelin]

Hmmm... can't notation help us there?
I claim that every mathematician understands in a few minutes that higher monoids don't have proof irrelevance for their associativity etc... (in fact there are even multiple generalisations)

[Scott Olson]

Is that much more to ask than understanding Prop vs. Type and universe levels?

[Mario Carneiro]

I think it is, mathematicians have no concept whatsoever about the higher structure of equality

[Johan Commelin]

There is an obvious definition of a group where you say Type instead, and it's not correct, and it will take you a while to realize this

It takes a while. But if you point out the analogy with actual homotopy theory, I think people get it fairly quickly.

[Mario Carneiro]

and now you've got people thinking about homotopy theory to do groups

[Johan Commelin]

I think it is, mathematicians have no concept whatsoever about the higher structure of equality

This is blatantly false for mathematicians coming from algebraic topology.

[Mario Carneiro]

I see I've targeted the wrong audience :)

[Johan Commelin]

Np, I think I'm getting your points.

[Johan Commelin]

So I repeat: Can't notation take care of this?

[Mario Carneiro]

The point is that HoTT makes you think about homotopy stuff whether you want to or not

[Johan Commelin]

Can't we have easy access to "Set"

[Mario Carneiro]

Maybe? It will still come up in proofs

[Mario Carneiro]

maybe you can automate that...

[Johan Commelin]

If it comes up in proofs after the definition, then this is probably for a good reason. Unless the computer should have been able to figure out is_Set or is_Prop on its own.

[Mario Carneiro]

but no one has really seriously attempted to "just do math" in HoTT AFAICT, except possibly UniMath. Everyone gets distracted by the abstract homotopy stuff

[Johan Commelin]

Right. I think I wouldn't get distracted. Neither would @Scott Morrison, @Patrick Massot or @Kevin Buzzard. We just want to take a far and high leap into normal classical research math.

[Mario Carneiro]

Quotient modules in UniMath: https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/Modules/Quotient.v

[Johan Commelin]

Do these rings and modules live in "Set", or are they higher order?

[Mario Carneiro]

looking at it, I don't see anything really out of place for regular math in Coq

[Mario Carneiro]

their setup for modules looks much less nice than lean's: https://github.com/UniMath/UniMath/blob/master/UniMath/Algebra/Modules/Core.v

[Mario Carneiro]

Ooh, a hott-ism:

(** The type of linear functions M -> N is a set. *)
Lemma isasetlinearfun {R : ring} (M N : module R) : isaset (linearfun M N).
Proof.
  intros. apply (isasetsubset (@pr1linearfun R M N)).
  - change (isofhlevel 2 (M -> N)).
    apply impred.
    exact (fun x => setproperty N).
  - refine (isinclpr1 _ _).
    intro.
    apply isapropislinear.
Defined.

[Johan Commelin]

They lack the pretty notation. But maybe that's because they don't distinguish between has_mul and has_add? Otherwise it looks pretty normal?

[Johan Commelin]

Ooh, let me see what you found.

[Scott Olson]

I think it makes sense that HoTT represents too big a shift in thinking about equality to be a drop-in replacement. I've gotten the impression that they hope it will help us do a lot of (non-homotopy...) math in a better way, but if it's a new way of doing math it couldn't be for the working mathematician until the working mathematician starts doing math differently

[Johan Commelin]

@Mario Carneiro Maybe that could have been proven by obviously...

[Scott Olson]

But it seems like that's still mainly hopes and works in progress. I'm curious to what extent they could eventually move away from homotopy terminology to make it more approachable to the mainstream

[Johan Commelin]

@[derive is_Set] def linearfun ... and automation derives it for you. I don't see anything blocking this...

[Mario Carneiro]

I think even dependent type theory is a hard sell what with the casts and hard types and such... HoTT adds even more irrelevant junk from the mathematicians POV

[Johan Commelin]

Right, I think no mathematician would want HoTT without univalence. But univalence is very enticing. And it might be worth the hurdles.

[Mario Carneiro]

But speaking of automation, we started on this discussion because we wanted to do transport of structure and anything HoTT can do using univalence we can do with a tactic

[Johan Commelin]

But speaking of automation, we started on this discussion because we wanted to do transport of structure and anything HoTT can do using univalence we can do with a tactic

Seriously? That sounds cool!

[Johan Commelin]

@Kevin Buzzard :up: voila!

[Johan Commelin]

We only need to get that tactic and you'll never hear us talking about HoTT or univalence again.

[Mario Carneiro]

It's not like it's an unsolved problem... that paper that was linked earlier seems to explain it in detail

[Mario Carneiro]

https://hal.inria.fr/hal-01559073v2/document

[Mario Carneiro]

But I also wanted to cure you of the idea that HoTT would magically solve these problems

[Mario Carneiro]

You still have to prove that all your notions respect equality, it's just expressed differently

[Mario Carneiro]

you need to prove how transport computes on a bunch of things, and this is where the work is

[Mario Carneiro]

I think we should try again with transfer and see what goes wrong

[Johan Commelin]

Still, I hope that such a tactic would significantly decrease the length and mental overhead of Bryan's proof that equivalent sets have equivalent partitions.

[Johan Commelin]

Right, but currently transfer seems a framework that doesn't have any tactics to guide mere mortal mathematicians through it.

[Mario Carneiro]

You need to prove that equivs respect filter and powerset... it's not that difficult

[Johan Commelin]

I've tried a couple of times, but got stuck all the time.

[Mario Carneiro]

The key is to prove those relators for lots of interesting notions

[Mario Carneiro]

transfer is useless without them

[Johan Commelin]

Right. We need a (general) tactic that would generate those two goals (in this specific case)

[Mario Carneiro]

no, you need to prove them

[Mario Carneiro]

they are not trivial claims

[Mario Carneiro]

but transfer will glue them together into larger proofs

[Johan Commelin]

No, I mean it takes the main goal. I invoke univalence. And it splits into the two goals you mentioned. Then I prove those.

[Johan Commelin]

So we're talking about the same thing.

[Mario Carneiro]

Ideally the lemmas about powerset and filter will already be in the library

[Johan Commelin]

Currently there is no tactic called transfer, right?

[Mario Carneiro]

there is

[Johan Commelin]

Ideally the lemmas about powerset and filter will already be in the library

Sure... at some point they will be.

[Mario Carneiro]

it's in core

[Johan Commelin]

And if VScode has a mode "Turn current goal into lemma" I think we would generate those facts even faster. (Instead of hiding them as subproofs.)

[Mario Carneiro]

they aren't hard theorems, but no one has tried to prove them, or more likely they are already there but without the peculiar notation

[Scott Olson]

You still have to prove that all your notions respect equality, it's just expressed differently
you need to prove how transport computes on a bunch of things, and this is where the work is

this was my impression when looking into cubical type theory. for example, there univalence itself seems small and easy to prove, because the details are bound up in the more fundamental ideas of transport-respecting equality in the type theory

[Johan Commelin]

@Mario Carneiro What exactly would "equiv respects powerset" look like in Lean, to make it usable for transfer?

[Scott Olson]

you also get things like how equalities between pairs are actually equal to pairs of equalities between the two fields (with proof-relevant equalities), which maps to how transporting pairs requires transporting each of the fields

[Mario Carneiro]

right, you have to recurse through that stuff to prove your theorem about transport of partition, so in the end it's not much different from the recursion that transfer will do

[Mario Carneiro]

or more precisely, you know immediately that the partitions of A and B are isomorphic, but what that isomorphism does is not obvious

[Johan Commelin]

I see

[Johan Commelin]

@Mario Carneiro I know you are really busy. But I would love that after the module refactoring is done this issue would land somewhere near the top of your todo list. Turning transfer into something that we smoothly use on a daily basis would be a huge win.

[Kevin Buzzard]

@Mario Carneiro here is a practical question. Once I said "oh we need ring". I probably said it about three times. And then one day I woke up and found that all of a sudden we had ring. My impression (correct me if I'm wrong) was that once you got down to it, it was just a cool project that maybe took you a weekend of coding because you understood exactly what needed to be done and then you just sat down and did it.

Well, now we "need" (in the same sense) the fact that if A and B are equiv topological rings then Spa A and Spa A are equiv topological spaces equipped with presheaves of topological rings, and to a mathematician the proof is rw h where h is the equiv. I fully understand that in Lean life is not so easy. But is this a tactic which will randomly just appear one day in mathlib like ring did or is this a far more serious research project? If it is I am wondering whether it is worth making it an issue for mathlib, so we know where we are and what needs doing. It would not surprise me if mathematicians have got big ideas about what this tactic is supposed to be doing, and I have no real feeling for whether Lean is capable of doing what we actually want, or whether Lean 4 changes things.

I have this mathlib issue which is not really an "issue" -- "let's define the adeles!". I am about to close it and put it instead on the "list of stuff which we should formalise at some stage". But my troubles with module are an issue I think, and non-existence of transfer is another issue. Is this a sensible usage of the "issue" functionality of github?

[Johan Commelin]

@Floris van Doorn @Cyril Cohen I heartily invite you to read through this thread and share some of your insights and expertise with us.

[David Michael Roberts]

What does univalence actually say?

perhaps I'm too late, but there's this explanation with Agda code http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html (see also the arXiv version https://arxiv.org/abs/1803.02294)

[David Michael Roberts]

@Scott Morrison yes, there are programs that have been extracted, but they are so slow and memory-hungry they cannot be run to completion, even to calculate Brunerie's number (which is known to be 2 even in HoTT, on paper)

[Floris van Doorn]

Thanks for the ping, Johan.
I think Mario has said most things already, but let me reiterate some points.

In HoTT you can develop ordinary mathematics. It will be mostly the same as formalizing things in mathlib. If you stay in the fragment of sets in HoTT, things will look very familiar. Here with "set" I mean a type A where for all a b : A the type a = b is a subsingleton (what we would call a propositon).

Disadvantages
There will be some disadvantages/inconviences when doing set-level mathematics in HoTT:

• You won't have definitional proof irrelevance. Even if you are working with sets, if you have two equalities h1 h2 : a = b, h1 and h2 will not be definitionally equal.
• You will have to prove that the objects you're dealing with are a set or proposition. For example: it is a lemma that n ≤ m is a proposition for natural numbers n and m. This is definitely automatable in 99% of the cases.
• classical.choice is inconsistent. The law of excluded middle and the axiom of choice are consistent with HoTT (and HoTT is no more tied to constructive mathematics than ordinary type theory is), as long as you restrict LEM to propositions (subsingletons) and the axiom of choice to sets. The restriction of classical.choice to a subsingleton type is consistent (and actually provable) in HoTT.
• Instead of a single universe of propositions, there is a subuniverse of propositions (defined as Prop := subtype is_prop as Johan suggested above) inside every universe. This means that if you talk about a proposition, you have to decide in which universe that proposition lives. This hasn't come up as a problem in the HoTT library yet, but could lead to the insertion of some ulifts.

I think the main reason why mathlib doesn't use HoTT is that we don't want to explain HoTT to all users of mathlib. Type theory is already weird enough for mathematicians, I think explaining the higher groupoid structure of equality would be too much. I think for experts, formalizing mathematics in HoTT won't be any harder than doing it in mathlib, but there will be a steeper learning curve. For example, if you have an element ⟨a, H⟩ : subtype P, and you apply a lemma which expects the term ⟨a, H'⟩ (same element, different proof of P a), you will get a type error. It's easy to fix this, but very confusing for an average user (⟨a, H⟩ = ⟨a, H'⟩ is provable by subtype_eq rfl).

Univalence
As mentioned before, univalence roughly states that if you have an equivalence between two types, then they are equal. More formally, it states that the function (A = B) → (A ≃ B) (which is easily defined by - for example - eq.rec) is itself an equivalence. One pedantic remark here is that stating that a function f : A → B is an equivalence (is_equiv f) is defined slightly different in HoTT than in mathlib. One important property we need is that is_equiv f is a subsingleton, and the type Σ(g : B → A), g ∘ f = id × f ∘ g = id is not. There are many definitions which do satisfy this property, the simplest is by saying that f has a left-inverse and f has a right-inverse, so (Σ(g : B → A), g ∘ f = id) × (Σ(h : B → A), f ∘ h = id). To be clear: there is a bi-implication between these two different definitions, but only the second one is a subsingleton, while the first one is not.

While univalence is only a statement about types, we can then prove it for all kinds of other structures: the type of equalities (G = H) between groups correspond to the type of group isomorphism between G and H. Equalities (C = D) between categories correspond to isomorphism of categories (and if C and D are so-called univalent categories, then it also corresponds to equivalence of categories), etc.

Univalence allows you to transport definitions and theorems between isomorphic structures. The catch is that if univalence is an axiom, these transported definitions will not be definitionally equal to what you want/expect (in cubical type theory it is, see below). As long as you are working with set-level objects, this will not be a problem. You can easily prove that the transported definition is equal to what you expect (and this is definitely automatable with a tactic). When transporting theorems, this will not be a problem, since we don't care about how we've proven these theorems.
Let's look at two examples. In both cases I have a group G, a subgroup H of G and have proven that the property PH : P H holds. Now suppose ϕ is a group isomorphism from G to G'

• It is easy to now find a subgroup H' of G' such that P H' holds. Just transport ⟨H, PH⟩ along the equality G = G' obtained from the group isomorphism. It is a lemma that H' is the image of H under ϕ.
• Suppose we already have defined a subgroup H' of G'. To show that P H' holds, we can show that H' is the image of H under ϕ. We can then use univalence to get P H'. This will require some reasoning steps, but I'm sure that this can be automated using a tactic.

Cubical Type Theory
In cubical type theory univalence does compute. The disadvantage is that the type theory is a lot more complicated and under active research. For example, for many variants of cubical type theory meta-theoretic properties like canonicity and decidable type-checking are still open. Reducing a couple instances of univalence will be fast and efficient. In this way it's nothing like computing Brunerie's number. Computing Brunerie's number is slow in the same way that kernel reduction in Lean is slow: you wouldn't want to compute 2^100 using kernel computation, but reducing a couple of beta-redexes with the kernel is fine.

I hope this answers some questions.

[Johan Commelin]

@Floris van Doorn Thanks a lot for this extensive reply!

[Kevin Buzzard]

Many thanks Floris! Your comments are very clarifying for me.

[Chris Hughes]

One thing about this I haven't managed to work out is how you can end up with two different proofs of equality that are provably not equal. Are there any simple examples?

[Floris van Doorn]

There are two ways:
(1) Using the univalence axioms, equality between types A and B correspond to (more precisely: are equivalent to) equivalences between A and B. So for example, for every bijection between nat and int you get an equality between nat and int, and these are provably unequal the corresponding bijections are unequal.

(2) In HoTT, you can extend the language with Higher Inductive Types. These are like inductive types, where your constructors can be either new elements of the type you're constructing, but also new paths (equalities) between the elements.
For example, you can have an interval I with three constructors:

• zero : I
• one : I
• segment : zero = one

This is a trivial example, where we get a type with two points, and a path from zero to one. A more interesting example is the circle with two constructors:

• base : circle
• loop : base = base

Using the univalence axiom you can prove that loop is not equal to refl base. Moreover, you can prover that the type base = base is equivalent to the type int. (the map int -> base = base sends n to loop ^ n.)

Another higher inductive type you know is quotient in Lean 3. For quotient A you have two constructors:

• A point constructor quotient.mk : A -> quotient A
• A path constructor quotient.sound : \forall (a b : A), a ~ b -> mk a = mk b

If you want to define this quotient in HoTT you want to add an additional constructor with type\forall (a b : quotient A) (p q : a = b), p = q. This enforces that the resulting type is in fact a "set": a type where any two proofs of the same equality are in fact equal.

[Floris van Doorn]

For all higher inductive types you get an induction principle/recursion principle like foo.rec in Lean. It roughly states that to define a function out of a higher inductive type, you have to say to what elements you have to send the point constructors, and show that the map respects the path constructors. For quotient, this corresponds exactly to quotient.lift and quotient.rec. And for the circle, you have to use this principle to show that loop != refl base.

[Johan Commelin]

@Chris Hughes The example about circle is very good. In general topology (or homotopy theory) gives good intuition for HoTT. (What's in a name?)
Have you seen fundamental groups in topology yet? Then you will have seen homotopies (continuously deforming a path into another path). And of course we want to call two paths in a topological space "equal" if they are homotopic. Any two homotopies between two paths p_1 and p_2 will be proofs that p_1 = p_2, but of course those homotopies don't have to be equal.
In ordinary maths we are using setoids and quotients for all of this. (So instead of homotopies, I could have talked about equality in quotient groups instead...) The difference in homotopy theory is that we don't actually want to take the quotient. We want to remember the homotopies. And we also want to remember homotopies between homotopies. HoTT allows us to do this synthetically in the type theory. It is thus suited very well for higher-categorical reasoning in mathematics (and for synthetic homotopy theory).

[Chris Hughes]

I have googled the definition of fundamental group, but I don't know much more than that about them. I understand it well enough to understand most of the analogies given when reading about HoTT, but I had no idea why they were relevant to Type theory until now. I think I'll have to read up on higher inductive types. Thanks @Floris van Doorn