[Agda] Strict equality _≣_ in agda

[Herminie Pagel]

Thank you all for the answers!

I agree with that old chinese wisdom, stacked dashes are a very good visual
metaphor. Even Apple is using it in their gestures! :)

@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?

@Thorsten Is there a sequel to that paper?

@Jesper Is your implementation available? Does it work with 2.6.1? I could
not find it in your github.

I also found Paolo's presentation
<http://csl16.lif.univ-mrs.fr/static/media/talk26/sstypes-slides-capriotti.pdf>
if someone is interested.

Best,

-- h

Am Di., 21. Apr. 2020 um 10:55 Uhr schrieb Thorsten Altenkirch <
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> 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/92a64f08/attachment.html>