[Agda] Tips for working around proof relevance

[James Wood]

On 20/12/2020 17:04, Jacques Carette wrote:
> The reason for sym-assoc is for definitional equality. This way C.op.op
> is definitionally equal to C. Otherwise, it is merely propositionally
> equal, and this means that some things that normally typecheck in
> category theory no longer do.

The way stdlib is set up, you don't even get propositional equality 
without some extra work. With the naïve definition (i.e, the 
agda-categories definition without sym-assoc), we get that
   op (op C) .assoc f g h = sym (sym (C .assoc f g h)) .
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