[Agda] Strict equality _≣_ in agda

[Andreas Abel]

 > _≡_  as the identity type former?

Well, we use _≡_ for the Martin-Löf identity type, which has different 
interpretations in different flavors of type theory.  In Agda, we have 
these three:

   --with-K
   --without-K
   --cubical

Not sure whether this answers your question, though.
--Andreas

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