[Agda] [Coq-Club] Why dependent type theory?

[Kevin Buzzard]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200305/7295c728/attachment.html>