The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

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.