Zulip Chat Archive

Stream: general

Topic: what is wrong with HoTT


Johan Commelin (Oct 05 2018 at 16:34):

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 (Oct 05 2018 at 18:45):

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 (Oct 05 2018 at 18:48):

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

Chris Hughes (Oct 05 2018 at 18:49):

(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 (Oct 05 2018 at 18:50):

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 (Oct 05 2018 at 18:54):

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

Chris Hughes (Oct 05 2018 at 18:54):

What does univalence actually say?

Kevin Buzzard (Oct 05 2018 at 18:56):

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

Bryan Gin-ge Chen (Oct 05 2018 at 19:01):

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 (Oct 05 2018 at 19:03):

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

Chris Hughes (Oct 05 2018 at 19:03):

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 (Oct 05 2018 at 19:08):

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

Reid Barton (Oct 05 2018 at 19:09):

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

Johan Commelin (Oct 05 2018 at 19:44):

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 (Oct 05 2018 at 19:53):

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 (Oct 05 2018 at 19:55):

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 (Oct 05 2018 at 19:57):

@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 (Oct 05 2018 at 20:03):

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

Kevin Buzzard (Oct 05 2018 at 20:17):

Is that exactly the equiv?

Kevin Buzzard (Oct 05 2018 at 20:18):

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

Reid Barton (Oct 05 2018 at 20:20):

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 (Oct 05 2018 at 20:20):

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 (Oct 05 2018 at 20:22):

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

Kevin Buzzard (Oct 05 2018 at 20:23):

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

Reid Barton (Oct 05 2018 at 20:23):

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 (Oct 05 2018 at 20:23):

Because then you could just conclude that S = R.

Kevin Buzzard (Oct 05 2018 at 20:24):

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

Reid Barton (Oct 05 2018 at 20:24):

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

Chris Hughes (Oct 05 2018 at 20:26):

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

Kevin Buzzard (Oct 05 2018 at 20:26):

plus the typeclass on C

Kevin Buzzard (Oct 05 2018 at 20:27):

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

Andrew Ashworth (Oct 05 2018 at 20:29):

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 (Oct 05 2018 at 20:30):

But does that stop me from defining a perfectoid space?

Patrick Massot (Oct 05 2018 at 20:31):

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

Andrew Ashworth (Oct 05 2018 at 20:31):

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

Mario Carneiro (Oct 05 2018 at 21:08):

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 (Oct 05 2018 at 21:10):

(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 (Oct 05 2018 at 21:11):

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 (Oct 05 2018 at 21:17):

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 (Oct 05 2018 at 21:18):

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 (Oct 05 2018 at 21:21):

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 (Oct 05 2018 at 21:22):

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 (Oct 05 2018 at 21:22):

HoTT is inconsistent with proof irrelevance

Mario Carneiro (Oct 05 2018 at 21:22):

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

Mario Carneiro (Oct 05 2018 at 21:25):

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 (Oct 05 2018 at 21:26):

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 (Oct 05 2018 at 21:29):

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 (Oct 05 2018 at 21:30):

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 (Oct 05 2018 at 21:40):

"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 (Oct 05 2018 at 21:40):

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

Chris Hughes (Oct 05 2018 at 21:41):

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 (Oct 05 2018 at 23:03):

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

Reid Barton (Oct 05 2018 at 23:08):

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 (Oct 05 2018 at 23:28):

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 (Oct 06 2018 at 03:50):

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 (Oct 06 2018 at 03:52):

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

Mario Carneiro (Oct 06 2018 at 03:52):

choice is not

Mario Carneiro (Oct 06 2018 at 03:54):

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

Mario Carneiro (Oct 06 2018 at 03:56):

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 (Oct 06 2018 at 03:56):

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

Mario Carneiro (Oct 06 2018 at 03:59):

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 (Oct 06 2018 at 03:59):

just as constructive math is an occasional distraction here

Scott Olson (Oct 06 2018 at 04:02):

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 (Oct 06 2018 at 04:03):

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 (Oct 06 2018 at 04:04):

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 (Oct 06 2018 at 04:04):

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

Mario Carneiro (Oct 06 2018 at 04:04):

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 (Oct 06 2018 at 04:05):

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

Johan Commelin (Oct 06 2018 at 04:05):

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 (Oct 06 2018 at 04:05):

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

Johan Commelin (Oct 06 2018 at 04:06):

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 (Oct 06 2018 at 04:06):

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 (Oct 06 2018 at 04:07):

Oh, I missed that you said it was a prop

Johan Commelin (Oct 06 2018 at 04:07):

Sure, that makes all the difference.

Mario Carneiro (Oct 06 2018 at 04:07):

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

Scott Olson (Oct 06 2018 at 04:07):

props are defined as types whose path space is contractible

Mario Carneiro (Oct 06 2018 at 04:07):

and is_prop is basically subsingleton

Mario Carneiro (Oct 06 2018 at 04:08):

because there is no "universe of props"

Johan Commelin (Oct 06 2018 at 04:08):

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 (Oct 06 2018 at 04:09):

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 (Oct 06 2018 at 04:09):

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

Mario Carneiro (Oct 06 2018 at 04:10):

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

Johan Commelin (Oct 06 2018 at 04:10):

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 (Oct 06 2018 at 04:10):

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

Mario Carneiro (Oct 06 2018 at 04:12):

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

Mario Carneiro (Oct 06 2018 at 04:12):

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

Johan Commelin (Oct 06 2018 at 04:12):

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 (Oct 06 2018 at 04:13):

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

Benedikt did this for monoids in that talk.

Johan Commelin (Oct 06 2018 at 04:13):

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

Johan Commelin (Oct 06 2018 at 04:14):

And I'm using his notation.

Johan Commelin (Oct 06 2018 at 04:14):

But Set should probably be Type + is_set M

Mario Carneiro (Oct 06 2018 at 04:14):

I am alluding to the Set part

Mario Carneiro (Oct 06 2018 at 04:14):

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

Johan Commelin (Oct 06 2018 at 04:14):

Ok, what's wrong with it?

Mario Carneiro (Oct 06 2018 at 04:15):

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

Mario Carneiro (Oct 06 2018 at 04:16):

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 (Oct 06 2018 at 04:16):

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 (Oct 06 2018 at 04:16):

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

Mario Carneiro (Oct 06 2018 at 04:17):

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

Johan Commelin (Oct 06 2018 at 04:17):

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 (Oct 06 2018 at 04:17):

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

Johan Commelin (Oct 06 2018 at 04:17):

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 (Oct 06 2018 at 04:17):

I see I've targeted the wrong audience :)

Johan Commelin (Oct 06 2018 at 04:17):

Np, I think I'm getting your points.

Johan Commelin (Oct 06 2018 at 04:18):

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

Mario Carneiro (Oct 06 2018 at 04:18):

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

Johan Commelin (Oct 06 2018 at 04:18):

Can't we have easy access to "Set"

Mario Carneiro (Oct 06 2018 at 04:18):

Maybe? It will still come up in proofs

Mario Carneiro (Oct 06 2018 at 04:18):

maybe you can automate that...

Johan Commelin (Oct 06 2018 at 04:19):

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 (Oct 06 2018 at 04:19):

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 (Oct 06 2018 at 04:20):

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 (Oct 06 2018 at 04:20):

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

Johan Commelin (Oct 06 2018 at 04:21):

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

Mario Carneiro (Oct 06 2018 at 04:21):

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

Mario Carneiro (Oct 06 2018 at 04:23):

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 (Oct 06 2018 at 04:25):

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 (Oct 06 2018 at 04:25):

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 (Oct 06 2018 at 04:25):

Ooh, let me see what you found.

Scott Olson (Oct 06 2018 at 04:26):

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 (Oct 06 2018 at 04:26):

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

Scott Olson (Oct 06 2018 at 04:28):

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 (Oct 06 2018 at 04:28):

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

Mario Carneiro (Oct 06 2018 at 04:28):

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 (Oct 06 2018 at 04:30):

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

Mario Carneiro (Oct 06 2018 at 04:30):

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 (Oct 06 2018 at 04:30):

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 (Oct 06 2018 at 04:31):

@Kevin Buzzard :up: voila!

Johan Commelin (Oct 06 2018 at 04:31):

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

Mario Carneiro (Oct 06 2018 at 04:31):

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

Mario Carneiro (Oct 06 2018 at 04:31):

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

Mario Carneiro (Oct 06 2018 at 04:33):

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

Mario Carneiro (Oct 06 2018 at 04:33):

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

Mario Carneiro (Oct 06 2018 at 04:34):

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

Mario Carneiro (Oct 06 2018 at 04:34):

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

Johan Commelin (Oct 06 2018 at 04:35):

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 (Oct 06 2018 at 04:36):

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

Mario Carneiro (Oct 06 2018 at 04:36):

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

Johan Commelin (Oct 06 2018 at 04:36):

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

Mario Carneiro (Oct 06 2018 at 04:36):

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

Mario Carneiro (Oct 06 2018 at 04:36):

transfer is useless without them

Johan Commelin (Oct 06 2018 at 04:36):

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

Mario Carneiro (Oct 06 2018 at 04:37):

no, you need to prove them

Mario Carneiro (Oct 06 2018 at 04:37):

they are not trivial claims

Mario Carneiro (Oct 06 2018 at 04:37):

but transfer will glue them together into larger proofs

Johan Commelin (Oct 06 2018 at 04:37):

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 (Oct 06 2018 at 04:37):

So we're talking about the same thing.

Mario Carneiro (Oct 06 2018 at 04:38):

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

Johan Commelin (Oct 06 2018 at 04:38):

Currently there is no tactic called transfer, right?

Mario Carneiro (Oct 06 2018 at 04:38):

there is

Johan Commelin (Oct 06 2018 at 04:38):

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

Sure... at some point they will be.

Mario Carneiro (Oct 06 2018 at 04:38):

it's in core

Johan Commelin (Oct 06 2018 at 04:39):

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 (Oct 06 2018 at 04:39):

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 (Oct 06 2018 at 04:40):

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 (Oct 06 2018 at 04:41):

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

Scott Olson (Oct 06 2018 at 04:42):

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 (Oct 06 2018 at 04:45):

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 (Oct 06 2018 at 04:46):

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 (Oct 06 2018 at 04:46):

I see

Johan Commelin (Oct 06 2018 at 05:12):

@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 (Oct 06 2018 at 11:46):

@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 (Oct 06 2018 at 15:14):

@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 (Oct 06 2018 at 23:48):

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 (Oct 06 2018 at 23:49):

@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 (Oct 07 2018 at 16:33):

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 (Oct 07 2018 at 17:00):

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

Kevin Buzzard (Oct 07 2018 at 20:47):

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

Chris Hughes (Oct 31 2018 at 16:53):

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 (Oct 31 2018 at 17:13):

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 (Oct 31 2018 at 17:17):

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 (Oct 31 2018 at 17:45):

@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 (Oct 31 2018 at 18:12):

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


Last updated: Dec 20 2023 at 11:08 UTC