[Agda] Strict equality _≣_ in agda

[Thorsten Altenkirch]

@Thorsten Is there a sequel to that paper?

Yes, there is

Two-Level Type Theory and Applications
Danil Annenkov<https://arxiv.org/search/cs?searchtype=author&query=Annenkov%2C+D>, Paolo Capriotti<https://arxiv.org/search/cs?searchtype=author&query=Capriotti%2C+P>, Nicolai Kraus<https://arxiv.org/search/cs?searchtype=author&query=Kraus%2C+N>, Christian Sattler<https://arxiv.org/search/cs?searchtype=author&query=Sattler%2C+C>
https://arxiv.org/abs/1705.03307


Am Di., 21. Apr. 2020 um 10:55 Uhr schrieb Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>>:
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<mailto:agda-bounces at lists.chalmers.se>> on behalf of Herminie Pagel <herminie.pagel at gmail.com<mailto:herminie.pagel at gmail.com>>
Date: Tuesday, 21 April 2020 at 08:04
To: Agda mailing list <agda at lists.chalmers.se<mailto: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.









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/20200422/7a576412/attachment.html>