<div dir="ltr"><div>Hi Herminie,</div><div><br></div><div>The prototype implementation of 2-level type theory I did during the Agda meeting is available at <a href="https://github.com/jespercockx/agda/tree/2ltt">https://github.com/jespercockx/agda/tree/2ltt</a>, there is some example code at <a href="https://github.com/jespercockx/agda/blob/2ltt/test/Succeed/SST.agda">https://github.com/jespercockx/agda/blob/2ltt/test/Succeed/SST.agda</a>. I haven't tested with 2.6.1, but it's likely some things have to be updated before it compiles.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 21, 2020 at 2:33 PM Herminie Pagel <<a href="mailto:herminie.pagel@gmail.com">herminie.pagel@gmail.com</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 dir="ltr"><div>Thank you all for the answers!</div><div><br></div><div>I agree with that old chinese wisdom, stacked dashes are a very good visual metaphor. Even Apple is using it in their gestures! :)</div><br>@Andreas As a side-effect, I have now a better understanding of the meaning of those agda flags. I know that K postulates that x ≡ x has exactly one element, but what do I assume/not assume when using --cubical?<br><br><div>@Thorsten Is there a sequel to that paper?</div><div></div><br><div>@Jesper Is your implementation available? Does it work with 2.6.1? I could not find it in your github.</div><div><br></div><div>I also found <a href="http://csl16.lif.univ-mrs.fr/static/media/talk26/sstypes-slides-capriotti.pdf" target="_blank">Paolo's presentation</a> if someone is interested. </div><div><br></div><div>Best,</div><div><br></div><div>-- h<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Am Di., 21. Apr. 2020 um 10:55 Uhr schrieb Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>>:<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>
<p class="MsoNormal"><span>I don’t think there is a standard definition of strict equality in Agda.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>It is possible to have both weak and strict equality in Agda as described in our paper<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"-webkit-standard",serif;color:black"><a href="http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf" target="_blank">Extending Homotopy Type Theory with Strict Equality</a></span><span style="font-family:"-webkit-standard",serif;color:black"><u></u><u></u></span></p>
<p class="MsoNormal"><span>At the last Agda meeting Jesper implemented some extension to the universe mechanism which allows us to have a universe of pretypes with strict equality and fibrant types with weak equality.
<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>The syntax of equality in agda is a bit confusing. In writing I would use = for the usual weak equality type and \equiv for either judgemental or strict equality. However, in agda it is the other
way around, because traditionally = is used in definitions and it has the advantage of being an ASCII character.
<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal" style="margin-left:36pt"><b><span style="font-size:12pt;color:black">From:
</span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Herminie Pagel <<a href="mailto:herminie.pagel@gmail.com" target="_blank">herminie.pagel@gmail.com</a>><br>
<b>Date: </b>Tuesday, 21 April 2020 at 08:04<br>
<b>To: </b>Agda mailing list <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>[Agda] Strict equality _</span><span style="font-size:12pt;font-family:"Cambria Math",serif;color:black">≣</span><span style="font-size:12pt;color:black">_ in agda<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12pt;margin-left:36pt">
Hi,<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-left:36pt">Is there a standard interpretation of the strict equality _<span style="font-family:"Cambria Math",serif">≣</span>_ (latex \===) in agda similar to the standard interpretation of _≡_ as the identity type former?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">best,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36pt">-- h<u></u><u></u></p>
</div>
</div>
</div>
<pre>This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
</pre></div>
</blockquote></div>
_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>