<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 4 Mar 2020 at 07:18, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dependent types are good for pure mathematics (classical or <br>
constructive). They are the natural home to define group, ring, metric <br>
space, topological space, poset, lattice, category, etc, and study them. <br>
Mathematicians that use(d) dependent types include Voevodsky (in Coq) <br>
and Kevin Buzzard (in Lean), among others. Kevin and his team defined, <br>
in particular, perfectoid spaces in dependent type theory. Martin<br></blockquote><div><br></div><div>The BCM (Buzzard, Commelin, Massot) paper defined perfectoid spaces in Lean</div><div>and looking forwards (in the sense of trying to attract "working mathematicians"</div><div>into the area of formalisation) I think it's an interesting question as to whether this definition</div><div>could be made in other systems in a way which is actually usable. My guess: I don't see why it couldn't</div><div>be done in Coq (but of course the type theories of Lean and Coq are similar), although</div><div>there is a whole bunch of noncomputable stuff embedded in the mathematics.<br></div><div>I *suspect* that it would be a real struggle to do it in any of the HOL systems</div><div>because a sheaf is a dependent type, but these HOL people are good at tricks</div><div>for working around these things -- personally I would start with seeing whether</div><div>one can set up a theory of sheaves of modules on a locally ringed space in a HOL</div><div>system, because that will be the first stumbling block. And as for the HoTT systems,</div><div>I have no feeling as to whether it is possible to do any serious mathematics other than</div><div>category theory and synthetic homotopy theory -- my perception is that</div><div>the user base are more interested in other kinds of questions. <br></div><div><br></div><div>In particular, connecting back to the original question, a sheaf of modules on a</div><div>locally-ringed space is a fundamental concept which shows up in a typical MSc</div><div>or early PhD level algebraic geometry course (they were in the MSc algebraic</div><div>geometry course I took), and if one wants to do this kind of mathematics in a</div><div>theorem prover (and I do, as do several other people in the Lean community)</div><div>then I *suspect* that it would be hard without dependent types. On the other hand</div><div>I would love to be proved wrong.<br></div><div><br></div><div>Kevin<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
On 03/03/2020 19:43, <a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a> wrote:<br>
> I'm in the process of writing my thesis on proof assistant performance <br>
> bottlenecks (with a focus on Coq), and there's a large class of <br>
> performance bottlenecks that come from (mis)using the power of dependent <br>
> types.  So in writing the introduction, I want to provide some <br>
> justification for the design decision of using dependent types, rather <br>
> than, say, set theory or classical logic (as in, e.g., Isabelle/HOL).  <br>
> And the only reasons I can come up with are "it's fun" and "lots of <br>
> people do it"<br>
> <br>
> So I'm asking these mailing lists: why do we base proof assistants on <br>
> dependent type theory?  What are the trade-offs involved?<br>
> I'm interested both in explanations and arguments given on list, as well <br>
> as in references to papers that discuss these sorts of choices.<br>
> <br>
> Thanks,<br>
> Jason<br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</blockquote></div></div>