[Agda] Why dependent type theory?

[Jason Gross]

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