<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
@font-face
{font-family:-webkit-standard;
panose-1:2 11 6 4 2 2 2 2 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;}
span.EmailStyle20
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">@Thorsten Is there a sequel to that paper?<o:p></o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Yes, there is <o:p></o:p></p>
<p class="MsoNormal"><b><o:p> </o:p></b></p>
<p class="MsoNormal"><b>Two-Level Type Theory and Applications<o:p></o:p></b></p>
<p class="MsoNormal"><a href="https://arxiv.org/search/cs?searchtype=author&query=Annenkov%2C+D">Danil Annenkov</a>, <a href="https://arxiv.org/search/cs?searchtype=author&query=Capriotti%2C+P">Paolo Capriotti</a>, <a href="https://arxiv.org/search/cs?searchtype=author&query=Kraus%2C+N">Nicolai
Kraus</a>, <a href="https://arxiv.org/search/cs?searchtype=author&query=Sattler%2C+C">Christian Sattler</a><o:p></o:p></p>
<p class="MsoNormal">https://arxiv.org/abs/1705.03307<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Am Di., 21. Apr. 2020 um 10:55 Uhr schrieb Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>>:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
I don’t think there is a standard definition of strict equality in Agda.<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
It is possible to have both weak and strict equality in Agda as described in our paper<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<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><o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
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.
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
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. <o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
Thorsten<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:36.0pt">
<o:p></o:p></p>
<div style="border:none;border-top:solid windowtext 1.0pt;padding:3.0pt 0cm 0cm 0cm;border-color:currentcolor currentcolor">
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
<b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;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:12.0pt;font-family:"Cambria Math",serif;color:black">≣</span><span style="font-size:12.0pt;color:black">_ in agda</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;margin-bottom:12.0pt;margin-left:72.0pt">
Hi,<o:p></o:p></p>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
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?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
best,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt">
-- h<o:p></o:p></p>
</div>
</div>
</div>
<pre style="margin-left:36.0pt">This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
<pre style="margin-left:36.0pt">and may contain confidential information. If you have received this<o:p></o:p></pre>
<pre style="margin-left:36.0pt">message in error, please contact the sender and delete the email and<o:p></o:p></pre>
<pre style="margin-left:36.0pt">attachment. <o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt">Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
<pre style="margin-left:36.0pt">necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
<pre style="margin-left:36.0pt">communications with the University of Nottingham may be monitored <o:p></o:p></pre>
<pre style="margin-left:36.0pt">where permitted by law.<o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
</div>
</blockquote>
</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></body>
</html>