The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

For reference, we (Kevin and the hott community) had a discussion
about canonical isomorphisms here:
https://groups.google.com/d/msg/homotopytypetheory/NhIhMd7SM_4/tKvejHGiAwAJ

On Tue, Mar 17, 2020 at 1:02 AM Kevin Buzzard 
<kevin.m.buzzard AT gmail.com>
 wrote:
>>
>> 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 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 just do not know whether we need it in "Fields Medal mathematics" or 
> whatever you want to call it, because so little "Fields Medal mathematics" 
> is being done in theorem provers. I have this other life when I am going 
> round maths departments arguing that current mathematical practice is 
> extremely unhygenic, producing example after example where I think that pen 
> and paper mathematics has got completely out of control. One thing I have 
> learnt from a couple of years of doing this is that most mathematicians are 
> (a) completely aware of the issues and (b) don't care. A mathematical 
> historian told me that in fact mathematics has often been like this, 
> basically saying that it is the nature of progress in mathematics research.
>
>> 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.
>
>
> Mathematics is an incredibly broad discipline nowadays, as you say, and 
> serious mathematics is being done in plenty of places other than 
> mathematics departments. The group of people I am trying to "represent", 
> not necessarily by being one of them, but at least by having what I think 
> is a good understanding of their desires, are those people who do not care 
> about any of these applications, and just want to prove stuff like the 
> p-adic Langlands conjectures, abstract conjectures saying that some class 
> of infinite-dimensional objects coming from analysis are related to actions 
> of an infinite group on some spaces coming from algebra -- results which I 
> personally suspect will never have any applications to anything, but which 
> are just intrinsically beautiful and are hence funded because part of the 
> funding system in mathematics firmly believes in blue sky research. The 
> people I'm talking about are beautifully caricatured in "The Ideal 
> Mathematician" 
> https://personalpages.manchester.ac.uk/staff/hung.bui/ideal.pdf by David 
> and Hersh (in fact I slightly struggle to see what is so funny about that 
> article because I so completely understand the point of view of the 
> mathematician). In fact the only difference between some of the 
> mathematicians I know doing "Fields Medal mathematics" and the "ideal 
> mathematician" described in that article is that the areas the "Fields 
> Medal mathematicians" actually work in areas which are taken *much* more 
> seriously (like the p-adic Langlands philosophy), with very big communities 
> containing powerful people who are making big decisions about where the 
> funding is going within pure mathematics. These people might seem very 
> extreme to many of the people reading these mailing lists -- most do not 
> care about computation or constructivism, they spend their lives doing 
> classical reasoning about intrinisically infinite objects, and they do not 
> see the point of these proof assistants at all (and they also do not care 
> about bugs in computer code because the only point of the computer is to 
> check a gazillion examples to convince us that our deep conjectures are 
> true, and we know they're true anyway). The reason that the computer proof 
> community should be bending over backwards to accommodate these people is 
> that *these people are the important ones* within pure mathematics, and 
> many of them have very entrenched ideas about what is and isn't 
> mathematics, and what is and what isn't important. Thorsten makes some 
> excellent points about all the other places where mathematics is being used 
> but it's the people at the top of this particular tree who I want. It is 
> these people who should be telling us what kind of type theory should be 
> being used, at least for the system or systems that I believe they will 
> ultimately adopt. But until they notice that the systems exist it is very 
> difficult to get clear answers -- or indeed any answers.
>
> > As I said to me it seems that too much surface stuff is moved into the 
> > core of systems like Lean.
>
>
> What Lean has going for it is that in practice it is turning out to be very 
> easy to quickly formalise the kind of mathematics which these "top of the 
> tree" pure mathematicians care about. However this might be because of some 
> social phenomena rather than because of its underlying type theory.
>
>
> Kevin
>
>
>
>
>
>
>
>
> Thorsten
>
> On 08/03/2020, 14:25, "Agda on behalf of Bas Spitters" 
> <agda-bounces AT lists.chalmers.se
>  on behalf of 
> b.a.w.spitters AT gmail.com>
>  wrote:
>
>     Dear Kevin,
>
>     The excitement about HoTT is that it has brought together several
>     communities. Some are interested in homotopy theory and higher
>     category theory, some (like Vladimir) want a new foundation for modern
>     mathematics.
>     Some combine those two by higher toposes.
>
>     Some are trying to improve the previous generation of proof
>     assistants. E.g. this influenced the design of quotients types in
>     lean.
>     By Curry-Howard this also influences the design of programming
>     languages, like the cubical agda programming language
>     (https://pure.itu.dk/portal/files/84649948/icfp19main_p164_p.pdf)
>
>     If we consider HoTT as an extension of type theory with the univalence
>     axiom, then *of course* everything that was done before can still be
>     done.
>     E.g. the proof of Feit-Thompson is constructive and thus also works in
>     HoTT. (I can elaborate on this if needed.)
>
>     In fact, classical logic is valid in the simplicial set model
>     (https://www.math.uwo.ca/faculty/kapulkin/notes/LEM_in_sSet.pdf).
>     Moreover, that model also interprets strict propositions, so one could
>     even extend lean with univalence (I believe).
>     It would be interesting to know whether this simplifies the definition
>     of perfectoid spaces.
>
>     Best regards,
>
>     Bas
>
>     On Thu, Mar 5, 2020 at 12:25 PM Kevin Buzzard 
> <kevin.m.buzzard AT gmail.com>
>  wrote:
>     >
>     >
>     >
>     > On Wed, 4 Mar 2020 at 07:18, Martin Escardo 
> <m.escardo AT cs.bham.ac.uk>
>  wrote:
>     >>
>     >> Dependent types are good for pure mathematics (classical or
>     >> constructive). They are the natural home to define group, ring, 
> metric
>     >> space, topological space, poset, lattice, category, etc, and study 
> them.
>     >> Mathematicians that use(d) dependent types include Voevodsky (in Coq)
>     >> and Kevin Buzzard (in Lean), among others. Kevin and his team 
> defined,
>     >> in particular, perfectoid spaces in dependent type theory. Martin
>     >
>     >
>     > The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces 
> in Lean
>     > and looking forwards (in the sense of trying to attract "working 
> mathematicians"
>     > into the area of formalisation) I think it's an interesting question 
> as to whether this definition
>     > could be made in other systems in a way which is actually usable. My 
> guess: I don't see why it couldn't
>     > be done in Coq (but of course the type theories of Lean and Coq are 
> similar), although
>     > there is a whole bunch of noncomputable stuff embedded in the 
> mathematics.
>     > I *suspect* that it would be a real struggle to do it in any of the 
> HOL systems
>     > because a sheaf is a dependent type, but these HOL people are good at 
> tricks
>     > for working around these things -- personally I would start with 
> seeing whether
>     > one can set up a theory of sheaves of modules on a locally ringed 
> space in a HOL
>     > system, because that will be the first stumbling block. And as for 
> the HoTT systems,
>     > I have no feeling as to whether it is possible to do any serious 
> mathematics other than
>     > category theory and synthetic homotopy theory -- my perception is that
>     > the user base are more interested in other kinds of questions.
>     >
>     > In particular, connecting back to the original question, a sheaf of 
> modules on a
>     > locally-ringed space is a fundamental concept which shows up in a 
> typical MSc
>     > or early PhD level algebraic geometry course (they were in the MSc 
> algebraic
>     > geometry course I took), and if one wants to do this kind of 
> mathematics in a
>     > theorem prover (and I do, as do several other people in the Lean 
> community)
>     > then I *suspect* that it would be hard without dependent types. On 
> the other hand
>     > I would love to be proved wrong.
>     >
>     > Kevin
>     >>
>     >>
>     >> On 03/03/2020 19:43, 
> jasongross9 AT gmail.com
>  wrote:
>     >> > I'm in the process of writing my thesis on proof assistant 
> performance
>     >> > bottlenecks (with a focus on Coq), and there's a large class of
>     >> > performance bottlenecks that come from (mis)using the power of 
> dependent
>     >> > types.  So in writing the introduction, I want to provide some
>     >> > justification for the design decision of using dependent types, 
> rather
>     >> > than, say, set theory or classical logic (as in, e.g., 
> Isabelle/HOL).
>     >> > And the only reasons I can come up with are "it's fun" and "lots of
>     >> > people do it"
>     >> >
>     >> > So I'm asking these mailing lists: why do we base proof assistants 
> on
>     >> > dependent type theory?  What are the trade-offs involved?
>     >> > I'm interested both in explanations and arguments given on list, 
> as well
>     >> > as in references to papers that discuss these sorts of choices.
>     >> >
>     >> > Thanks,
>     >> > Jason
>     >> >
>     >> > _______________________________________________
>     >> > Agda mailing list
>     >> > 
> Agda AT lists.chalmers.se
>     >> > https://lists.chalmers.se/mailman/listinfo/agda
>     >> >
>     >>
>     >> --
>     >> Martin Escardo
>     >> http://www.cs.bham.ac.uk/~mhe
>     >
>     > --
>     > You received this message because you are subscribed to the Google 
> Groups "lean-user" group.
>     > To unsubscribe from this group and stop receiving emails from it, 
> send an email to 
> lean-user+unsubscribe AT googlegroups.com.
>     > To view this discussion on the web visit 
> https://groups.google.com/d/msgid/lean-user/CAH52Xb0X%3D06U2O7K%2BLGRXyPu%3DhaKxp2FcQr3SFK0f4jm8kv9mQ%40mail.gmail.com.
>     _______________________________________________
>     Agda mailing list
>     
> Agda AT lists.chalmers.se
>     https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
>
> 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.
>
>
>
>> 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.
>>
>>
>>
> --
> You received this message because you are subscribed to the Google Groups 
> "lean-user" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to 
> lean-user+unsubscribe AT googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/lean-user/CAH52Xb2TFq%2BV6kwq22Nw%3DGSt4wAecB%2B7M7JKvrvb4OBds%3DRZQg%40mail.gmail.com.