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

[Thorsten Altenkirch]

Hey Thorsten,

On Thu, 12 Mar 2020 at 15:36, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:

[snip]
This is a shame because in many ways lean is a nice system but it is unusable if you want to do structural Mathematics.

I do not recognise your objection.

You should – it is basically the same as what I said in your talk in Nottingham (which was great btw).

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.

Hence my understanding of structural Mathematics is very simple: its objects are structures and equality of structures should be structural equality. E.g. equality of (univalent) categories should be equivalence of categories (Why univalent categories: because isomorphic objects should be equal).

I don’t know what Mathematics is actually happening in Maths departments but you seem to agree that it can be done in Type Theory, e.g. in Lean. Indeed, in a way Type Theory is not far away from Mathematical practice (if we ignore the question of constructiveness for the moment). And it is different from set theory in that it structural by nature. I just find it strange if one cannot go the last step and exploit this fact. It seems somehow this is a blast from the past: because we cannot have univalence in set theory we don’t need it in type theory either?

I agree that equality between types is an issue in Lean. What I do not understand is why this matters to mathematicians in practice. Since "working mathematicians" became involved with using Lean the collection of mathematical structures formalised in Lean and theorems about these structures has gone through the roof. Lean as a powerful and exponentially growing classical mathematical library, which covers essentially all of a first year undergraduate mathematics curriculum and is well over half way through the second year, as well as being much more advanced (MSc level) in other areas such as algebra. Maybe I just don't know what "structural mathematics" is, but Lean is certainly usable if you want to do the kind of mathematics which is actually happening in mathematics departments. I am hopeful that one day this will happen with one of the HoTT systems but at the minute the only areas where they appear to go deep are synthetic homotopy theory and category theory, topos theory, abstract higher category theory etc. I have this nagging worry that away from these areas the univalence axiom (and the way it seems to rule out Lean's powerful impredicative Prop and a useful equality taking values in that Prop)

I am not aware that an impredicative Prop is inconsistent with HoTT. Indeed, Voevodsky put forward resizing which is equivalent to having an impredicative universe.

is more than a hindrance than a help. But I would love to be proved wrong. One thing that absolutely needs emphasizing is that classical logic is absolutely embedded in an undergraduate mathematics degree nowadays, and no "working mathematician" will take you seriously if you try to remove it. This is apparently an uncomfortable fact for some in the  community but it is one which I think it is important to remind people of; mathematics departments went classical in several central areas, many many decades ago, and we are not going back. Yes I know the proof of the odd order theorem is constructive. And we don't care. This is a statement about finite objects and unrepresentative of what is actually happening in 2020.

Ok, this is a different topic (and I didn’t say anything about constructive Maths in my original posting). I think the sort of Maths you are doing is very much influenced by what you are using it or what it has been used for in the past. It seems to me that until recently natural science and hardware engineering was the main application of Mathematics and hence influenced what Mathematicians considered as important. The world is changing and computer science and information technology are becoming an important application of Mathematics. For historical reasons and also for reasons of funding a lot of the Maths for Computer Science is actually done at Computer Science departments. I am just thinking that you, the Mathematicians, maybe miss a trick here; and so do we, the Computer Scientists because we could profit more from the wisdom of Mathematicians like yourself.

I think that Isabelle/HOL and HOL Light are evidence that for lots of mathematics (especially much of 19th and early 20th century mathematics) one does not even need dependent types, but I have this idea (again which I would love to be wrong about) suggesting that MSc level algebraic geometry and homological algebra are just too inconvenient to use without dependent types. In Lean we are moving onto Ext and Tor in the category of R-modules. I think it would be an extremely interesting project to see how these worked in practice in other systems.

Going further -- what is absolutely clear is that to get a better understanding of what the truth actually is, regarding the difficulty formalising the actual mathematics going on in mathematics departments in central areas such as algebra, geometry, number theory, analysis etc, we need *actual data*. We need libraries which correspond to what is being taught in mainstream undergraduate mathematics courses, in all the systems, if we want to see what the actual truth is. Sure every undergraduate pure maths course can be formalised in every system, in theory. But can it be formalised in finite time in a usable way in practice? This is what we simply do not know and I believe that we can only find out by getting more working mathematicians on board.

An interesting test with Lean will be what happens when Lean 4 is released. Lean 4 will not be backwards compatible with Lean 3 so the library will have to be ported from scratch, and it's got pretty big. The underlying type theory is not changing but the type class inference system is changing completely, and typeclasses are everywhere in Lean's maths library.

I should finish by taking the time to advertise Gabriel Ebner's HoTT library in Lean 3: https://github.com/gebner/hott3 . It adds a [hott] attribute to the system and "disables" singleton elimination. What can one do with it? Nobody really knows. Maybe for you (Thorsten) it's the best of both worlds?

Maybe. As I said to me it seems that too much surface stuff is moved into the core of systems like Lean.

Thorsten





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/20200313/000d8e51/attachment.html>