[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

[Thorsten Altenkirch]

From: Kevin Buzzard <kevin.m.buzzard at gmail.com>
Date: Tuesday, 17 March 2020 at 00:02
To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
Cc: agda-list <agda at lists.chalmers.se>, Coq Club <coq-club at inria.fr>, "coq+miscellaneous at discoursemail.com" <coq+miscellaneous at discoursemail.com>, lean-user <lean-user at googlegroups.com>
Subject: Re: [Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

It seems to me that if you are working with structures, i.e. do structural Mathematics you need to understand what they are and they cannot be reduced to their encodings. Hence what is the equality of structures, if not their structural equality? If I remember correctly, in your talk at Nottingham you discussed a construction by Grothendieck where he used equivalence of structures as if it were equality. This seems to be an omission and you and your students were able to address this, I think by choosing a canonical representation. However, the funny thing was that you were using a system which doesn’t allow you to express any non-structural properties but because of the way equality is done in Lean you cannot exploit this.

There is something subtle going on which I do not really understand, but it would not surprise me if there are plenty of people on these lists who do. Our problem with formalising the work of Grothendieck was that he assumed that objects which were "canonically" isomorphic were in fact equal. Canonical isomorphism is this weasel word which mathematicians often do not define properly, but in this particular case (we had a proof of P(A) and I could not deduce a proof of P(B) when B was "canonically" isomorphic to A) we solved the problem by noticing that in this particular case "canonically isomorphic" meant "satisfied the same universal property". We then changed our proof of P(A) to prove instead P(anything satisfying the universal property defining A), and then we were OK. I think it is interesting that at the point in my talk when I explained this, I said "and we couldn't believe it -- our proof barely needed changing" and you laughed and said something like "of course it didn't!". We are mathematicians learning how mathematics works :-) But we did not go "full univalence", we did not argue that isomorphic objects were equal, we only needed that "canonically" isomorphic objects were equal. In my experience of mathematics, this is the principle which is used. My fear of univalence is that because it goes a bit further, and that extra step seems to rule out some basic principles used in Lean's maths library and hence makes a whole bunch of mathematical proofs far more inconvenient to write. I am still learning about theorem provers but am urging my community to start formalising mathematics and this sort of thing is one of many issues which deserves to be better understood -- certainly by mathematicians!

I am wondering whether this idea of “canonical isomorphism” is just a bit of a stop gap which comes from set-theoretic thinking. I was laughing because anything you can do in type theory is stable under structural isomorphism. Hence certainly proofs can be transported along structural isomorphism. I just wonder if you have two mathematical objects which have all the same properties, then what would you call them if not equal?

But more practically: indeed you are right if you accept this point (i.e. univalence) then you have to give up some properties of equality in particular that it is propositional, i..e a property. This can be annoying because it may mean that you have to deal with coherence issues when using equality, but I suspect you should be used to this. However, as long as you only deal with simple objects, i.e. as in the “world of numbers” everything is fine and nothing changes. It is only when you leave the realm of “set level Mathematics” and talk about structures (as in the Grothendieck example) you encounter equalities which are not propositions (but structures themselves).

However, here comes a technical issue, which I think is overrated. Namely, Lean uses strict equality (I think I introduced this in a paper in ’99 to deal with extensionality) which means any two proofs of a proposition, e.g. a set level equality are “definitionally equal”, i.e. the type system knows this. Now the problem is that being a proposition in HoTT is a proposition itself while for a strict Prop you need it to be a judgement, i.e. static. However, both concepts can coexist in the same system: you can have strict and weak Prop. The weak Prop gives you a subobject classifier but the strict Prop is more convenient to use and only gives you a quasi-topos, I think.

So I think you can have your cake and eat it.

Thorsten

P.S. I agree with all the rest and appreciate that you want to reach the top of the tree Mathematicans.



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200318/2efb07eb/attachment.html>