[Agda] Explicit definition.

[Naïm Favier]

You're trying to show that a given identity type in HITOrd is a set, which is true because every set is a groupoid:

   (λ i j → isSet→isGroupoid trunc _ _)

Note that you can just use indProp instead:

   ⊕unitr = indProp (trunc _ _) ? ?

On 04/03/2025 19:41, Serge Leblanc wrote:
> [Some people who received this message don't often get email from 33dbqnxpy7if at gmail.com. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]
> 
> Hi,
> 
> I can't seem to make an explicit definition of ⊕unitr in my example.
> 
> Can someone help me and explain my mistake?
> 
> Thanks.
> 
> -- 
> Serge Leblanc
> -------------------------
> gpg --search-keys 0xD2B8A2825F8DABB7
> GnuPG Fingerprint = 123E 9312 453A 8F8E 7FDB ABD7 D2B8 A282 5F8D ABB7
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda