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

[Miguel Pagano]

On Wed, 4 Mar 2020 at 06:42, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> First of all I don’t like the word “dependent type theory”. Dependent
> types are one important feature of modern Type Theory but hardly the only
> one.
>
>
>
> To me the most important feature of Type Theory is the support of
> abstraction in Mathematics and computer science. Using  types instead of
> sets means that you can hide implementation choices which is essential if
> you want to build towers of abstraction. Set theory fails here badly.
>
I've been involved in formalizations projects both in Agda and Isabelle/ZF.
In my experience in Isabelle/ZF one can hide some implementation details;
for instance, one can change the relation used for an inductive proof
without affecting the rest of the argument. On the other hand, the lack of
types was, at certain points, frustrating: the "typing" information should
be stated explicitly as hypotheses on each lemma.

One shortcoming in Agda is how to capture classes, as in "classes of models
of some equational theory": the issue (it might be my ignorance) is that
each concept has a level (there might be more than one level if the
construction is interesting) and one can at most "kind" but not type the
class of instances of that concept.

Best regards,
M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200305/4196acca/attachment.html>