Thinking about this, adapted from a tweet that was meant to infuriate
if e then true else false
Because it's equivalent to e
ofc, but really it's a case of:
if e then C[true] else C[false] === C[e]
But also:
if e then (if e then e1 else e2) else (if e then e3 else e4) === if e then e1 else e4
Or generally:
if e then C1[e] else C2[e] === if e then C1[true] else C2[false]
And finally:
C[if e then e1 else e2] === if e then C[e1] else C[e2]
✨ eta laws ✨
Oh I refound the tweet https://twitter.com/hmemcpy/status/1363871098824179714
At least, the first one is definitely an eta law, since it's the eliminator wrapped around constructors
The third one is a bit dangerous, since
e
gets evaluated first instead of whatever's in your context CI feel like the second one should arise from some congruence rules but I can't see how