Fork of Nils Danielsson's "equality" repo
root
- Container
- Equality
- H-level
- README
- Tree-sort
- Univalence-axiom
- .boring
- Bag-equivalence.agda
- Bijection.agda
- Category.agda
- Container.agda
- Equality.agda
- Equivalence.agda
- Fin.agda
- Function-universe.agda
- Groupoid.agda
- H-level.agda
- Injection.agda
- LICENCE
- Logical-equivalence.agda
- M.agda
- Preimage.agda
- Prelude.agda
- README.agda
- Structure-identity-principle.agda
- Surjection.agda
- Tree.agda
- Univalence-axiom.agda