Localcoequalizers#475

Merged

JacquesCarette merged 50 commits intoagda:masterfrom

tillrampe:localcoequalizers

Jun 23, 2025

Commits on May 30, 2025

The isomorphism between two coequalizers fits into a triangle
tillrampe
committed
Add a type/proposition expressing the existence of all coequalizers
tillrampe
committed
Import more properties of coequalizers and hide some definitions to avoid name clashes
tillrampe
committed
Add proof that split coequalizers are coequalizers
tillrampe
committed
Proof that a map between parallel pairs induces a map between the respective coequalizers
tillrampe
committed
Prove that a coequailzer remains coequalizer after replacing the objects by isomorphic one
tillrampe
committed
Prove that coequalizers commute with coequalizers
tillrampe
committed
Add a type/proposition expressing that a functor preserves coequalizers
tillrampe
committed
Add definition of a bicategory with local coequalizers
tillrampe
committed

Commits on May 31, 2025

Commits on Jun 1, 2025

Commits on Jun 5, 2025

Commits on Jun 11, 2025