search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
450 stars 138 forks source link

(C ≃ᶜ C') ≃ (C ≡ C') for univalent categories #1091

Closed marcinjangrzybowski closed 7 months ago

marcinjangrzybowski commented 8 months ago
felixwellen commented 7 months ago

This is really nice to have - thanks also for the improvements/refactorings!