Remove categories from agda-base.
Refactor equivalence of coherent iso and we.
Add singleton'.
Add trans isomorphism with computational content.
Add computational rules for funext.
Make trans-iso more computational.
Add propositional truncation.
Add < for natural numbers.