(C ≃ᶜ C') ≃ (C ≡ C') & univalent category of setoids - Githubissues

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

446 stars 136 forks source link

(C ≃ᶜ C') ≃ (C ≡ C') & univalent category of setoids #1084

Closed marcinjangrzybowski closed 7 months ago

marcinjangrzybowski commented 8 months ago

new modules:

Cubical/Categories/Category/Path.agda - Simple helper representation of Path between categories to deal with ineficiency in WeakEquivalence.agda
Cubical/Relation/Binary/Setoid.agda Setoid - Pair of hSet and propositional equivalence relation
Cubical/Categories/Instances/Setoids.agda - Univalent Category of Setoids with adjoint quadruple of functors from/to SET : Quot ⊣ IdRel ⊣ Forget ⊣ FullRel

additions:

Cubical/Categories/Adjoint.agda - added composiiton of adjunctions
Cubical/Categories/Equivalence/WeakEquivalence.agda - Equivalence of Categories is equivalent to Path between Univalent Categories
Cubical/Categories/Instances/Functors.agda - currying of functors is an isomorphism.
Cubical/Foundations/Transport.agda - transport-filler-ua = ua-gluePath
some other minor helpers

marcinjangrzybowski commented 7 months ago

I will reopen after spliting into more generic categorical stuff vs relations stuff vs setoids