search

b-mehta / topos

Topos theory in lean
56 stars 2 forks source link

Improve epi-mono factorisation #28

Open b-mehta opened 4 years ago

b-mehta commented 4 years ago

Currently it requires all coequalizers to exist, but it suffices to only have reflexive coequalizers