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

Thu Mar 12 17:22:38 CET 2020

Dear Thorsten,

I think you're on the right track about the idea that "proof irrelevance" for set-level stuff should in fact be only virtual and should instead be implemented by a nice tactic. As you know, we have spent a great deal of time investigating extensions of ITT with definitional proof irrelevance (for equality), and others have done so for SProp --- unfortunately, we have found that definitional proof irrelevance is actually very badly behaved _except_ in the presence of equality reflection. Section 8 of our recent paper explains the difficulties with proof irrelevance in ITT, even when you are only interested in sets: http://www.jonmsterling.com/pdfs/sag20.pdf. This is why I have been a bit dismayed by the rush to adopt things like SProp in all type theoretic proof assistants, at a time when most of us had not yet fully understood the problems.

For the reasons we describe in our paper, I now strongly believe that even for set-level mathematics, one must not adopt proof irrelevance into the core (neither for equality, nor for a universe of propositions). It should, as Thorsten advocates, be implemented as some kind of coherence tactic that is so sophisticated that the user never sees it happening. However, it will be up to us type theorists to design such a tactic --- it is not totally obvious that this can be done in a way that the people who have become accustomed to systems like Lean would consider acceptable. I think we should try.

Best,
Jon

On Thu, Mar 12, 2020, at 11:36 AM, Thorsten Altenkirch wrote:
> One problem here is that the equality one uses in Lean is the strict 
> equality which is definitionally proof-irrelevant. This is a nice 
> feature to have for set-level reasoning but it doesn't work on higher 
> levels, i.e. reasoning about structures. Which is where the main power 
> of HoTT is, equivalence is equality.
> 
> I think it should be possible to have both features, that is simulate 
> definitional proof-irrelevance which is basically "extensional" type 
> theory on the set level via a powerful tactic but don't put this. Into 
> the foundations of the proof system. This is a common problem that 
> decisions which should only affect the surface are turned into core 
> features. This is a shame because in many ways lean is a nice system 
> but it is unusable if you want to do structural Mathematics.
> 
> 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.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>