<div dir="ltr"><div><br></div><div>You can represent the syntax of pretty much every dependent and impredicative theory in Agda. However, that does not settle whether a particular proof or construction using a syntax is a) possible in base Agda b) feasible or convenient in base Agda.</div><div><br></div><div>System F and F-omega syntax is easy to represent in Agda, in either intrinsic or extrinsic manner. Showing consistency or normalization would require an impredicative universe in Agda, so that's not possible without postulating stuff, but even without that there are many interesting things which you could do with the syntax.<br></div><div><br></div><div>Predicative dependent type theories can be represented and proven consistent; <a href="http://www.cse.chalmers.se/~abela/popl18.pdf">this is</a> the most advanced development I know of which only uses native Agda features (in this case, induction-recursion). Note though that formal handling of dependent types tends to be highly technically challenging.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="color:rgb(0,0,0);font-family:Calibri,Helvetica,sans-serif;font-size:16px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">For dependent type itself, I do not think it's possible, due to Goedel's incompleteness theorem.<span> </span></span></blockquote><div><br></div><div>Gödel doesn't enter the picture in any of the developments I know of, because the metatheories are stronger than object theories, due to having inductive families and/or induction/recursion. Also, Gödel would only prevent consistency proofs, but doesn't preclude representing the syntax or doing a number of interesting things with it which don't imply consistency.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span style="color:rgb(0,0,0);font-family:Calibri,Helvetica,sans-serif;font-size:16px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">is Prop type in Coq is impredicative, and therefore the calculus underneath (caculus of inductive constructions, CIC) is stronger than calculus of constructions(CoC)</span></blockquote><div><br></div><div>CoC has impredicative base Set. </div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-04-05 5:01 GMT+02:00 Jason -Zhong Sheng- Hu <span dir="ltr"><<a href="mailto:fdhzs2010@hotmail.com" target="_blank">fdhzs2010@hotmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div id="m_4985169126494722728divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Helvetica,sans-serif" dir="ltr">
<p>my intuition was there is nothing special about system F, and all terms and types should be just able to fit into Set along. and indeed, someone has done the work:
<a href="https://github.com/sstucki/system-f-agda" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk61793" target="_blank">
https://github.com/sstucki/<wbr>system-f-agda</a><br>
</p>
<p><br>
</p>
<p>regarding stronger calculus, i do not see why they are not possible, except for dependent type itself(i.e. the strongest calculus of the cube). For example, it's straightforward to formalize Fsub in Coq:
<a href="https://github.com/plclub/metalib/tree/master/Fsub" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk708107" target="_blank">
https://github.com/plclub/<wbr>metalib/tree/master/Fsub</a></p>
<p><br>
</p>
<p>The modelling calculus of Scala, (dependent object types, DOT), for example, has type dependent types, type dependent values, and a weak form of value dependent types, which can also be proved with terms and types in Set:
<a href="https://github.com/samuelgruetter/dot-calculus" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk43114" target="_blank">
https://github.com/<wbr>samuelgruetter/dot-calculus</a> <a href="https://github.com/amaurremi/dot-calculus" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk586999" target="_blank">ht<wbr>tps://github.com/amaurremi/<wbr>dot-calculus</a><br>
</p>
<p><br>
</p>
<p>Though in Coq, the terms and types are defined in Set, which roughly corresponds to Set in Agda, and that hopefully means you won't need to go above Set 2 to prove it's sound.</p>
<p><br>
</p>
<p>For dependent type itself, I do not think it's possible, due to Goedel's incompleteness theorem. However, someone did it in Coq (which i've not checked, but, well, it's there)
<a href="https://github.com/coq-contribs/coq-in-coq" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk842179" target="_blank">
https://github.com/coq-<wbr>contribs/coq-in-coq</a> . The reason why it might be doable in Coq, is Prop type in Coq is impredicative, and therefore the calculus underneath (caculus of inductive constructions, CIC) is stronger than calculus of constructions(CoC).
Indeed, the author represents typ to be Prop because he had no choice. <a href="https://github.com/coq-contribs/coq-in-coq/blob/master/Types.v" class="m_4985169126494722728OWAAutoLink" id="m_4985169126494722728LPlnk584766" target="_blank">https://github.com/<wbr>coq-contribs/coq-in-coq/blob/<wbr>master/Types.v</a></p>
<p><br>
</p>
<p>Hope that helps.<br>
</p>
<p><br>
</p>
<div id="m_4985169126494722728Signature">
<div id="m_4985169126494722728divtagdefaultwrapper" dir="ltr" style="font-size:12pt;color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif,"EmojiFont","Apple Color Emoji","Segoe UI Emoji",NotoColorEmoji,"Segoe UI Symbol","Android Emoji",EmojiSymbols">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a id="m_4985169126494722728LPNoLP"></a></b></span></span></font> </div>
</div>
</div>
<hr style="display:inline-block;width:98%">
<div id="m_4985169126494722728divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.<wbr>se</a>> on behalf of How Si Yu <<a href="mailto:howseeu@gmail.com" target="_blank">howseeu@gmail.com</a>><br>
<b>Sent:</b> April 4, 2018 10:36:21 PM<br>
<b>To:</b> <a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a><br>
<b>Subject:</b> [Agda] Encoding higher lambda calculus in agda</font>
<div> </div>
</div><div><div class="h5">
<div class="m_4985169126494722728BodyFragment"><font size="2"><span style="font-size:11pt">
<div class="m_4985169126494722728PlainText">Hi,<br>
<br>
There are numerous implementations of untyped lambda calculus and<br>
simply typed lambda calculus in Agda online. However, I can't find any<br>
mention of encoding of other "higher" lambda calculus in the lambda<br>
cube like λ2 or λP in Agda. Is it because they are inherently<br>
impredicative and can't be represented in Agda?<br>
<br>
Thanks,<br>
Si Yu<br>
______________________________<wbr>_________________<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" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</div></div></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>