[Agda] Why dependent type theory?

[Martin Escardo]

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

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