[Agda] Strict equality _≣_ in agda

[Andreas Abel]

 > but what do I assume/not assume when using --cubical?

That is a long story.  One thing is that in --cubical, the identity type 
is a primitive (not a data), and you cannot match on refl.

On 2020-04-21 14:32, Herminie Pagel 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 
> <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.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>