[Agda] Tips for working around proof relevance

[Nicolai Kraus]

Jacques and James, thanks for the explanations!

On 20/12/2020 22:16, James Wood wrote:
> The way stdlib is set up, you don't even get propositional equality 
> without some extra work. 

Thanks for pointing this out. I wasn't aware of it.
Asking the equivalence relation to be valued in h-props would be the 
first step towards saturation in Peter's hierarchy. Adding groupoid 
coherence laws would likely become insufficient after a while.

Nicolai

> To get a propositional equality from this to C .assoc f g h, we would 
> need Setoid to give us some propositional equations. We could either 
> enforce that the equivalence relation is h-prop-valued (probably the 
> right thing) or add groupoid coherence laws. On top of that, we would 
> need function extensionality.
>
> In any case, we should at least get an equivalence of categories, 
> though I'm not sure how useful that is in practice in a non-univalent 
> setting. In general, I think it's an interesting phenomenon that we 
> can get ourselves into situations where judgemental equality is the 
> only hope. The other example I can think of is how you can have a 
> (badly behaved) category of Sets in plain Agda without using setoids 
> because _∘_ is judgementally unital and associative.
>
> James
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda