[Agda] Strict equality _≣_ in agda

[Jesper Cockx]

Hi Herminie,

The prototype implementation of 2-level type theory I did during the Agda
meeting is available at https://github.com/jespercockx/agda/tree/2ltt,
there is some example code at
https://github.com/jespercockx/agda/blob/2ltt/test/Succeed/SST.agda. I
haven't tested with 2.6.1, but it's likely some things have to be updated
before it compiles.

-- Jesper

On Tue, Apr 21, 2020 at 2:33 PM Herminie Pagel <herminie.pagel at gmail.com>
wrote:

> 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.
>>
>>
>>
>>
>> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200421/2e8089fd/attachment.html>