<div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 4 Mar 2020 at 06:42, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.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">





<div lang="EN-GB">
<div class="gmail-m_70743794804187804WordSection1">
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal">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.</p></div></div></blockquote><div><div>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.</div><div><br></div><div>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.<br></div><div><br></div><div>Best regards,</div><div>M.</div></div></div></div>