[Agda] Strict equality _≣_ in agda

[Thorsten Altenkirch]

I don’t think there is a standard definition of strict equality in Agda.

It is possible to have both weak and strict equality in Agda as described in our paper
Extending Homotopy Type Theory with Strict Equality<http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf>
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.

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.

Thorsten

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Herminie Pagel <herminie.pagel at gmail.com>
Date: Tuesday, 21 April 2020 at 08:04
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] Strict equality _≣_ in agda

Hi,
Is there a standard interpretation of the strict equality _≣_ (latex \===) in agda similar to the standard interpretation of _≡_  as the identity type former?

best,

-- h



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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200421/65dc44f3/attachment.html>