[Merged by Bors] - feat: port CategoryTheory.Quotient

[mpenciak]

---

[mo271]

currently there are errors in three parts:

• instance category
• functor_map_eq_iff
• lift_unique

[bottine]

I checked the names and things seem in order now. Two changes that I'd like confirmation on:

• There was a commented-out deriving … line with an instance later on and a porting note explaining that the deriving … line didn't work. I just removed that commented-out deriving line, since the porting note is sufficiently informative I believe.
• In the following definition of HomRel, the isEquiv constructor was in UpperCamelCase, but I thought it matched items one and five of the porting wiki so I changed it to lowerCamel, and now I'm thinking it should maybe just be is_equiv? it's confusing.

/-- A `HomRel` is a congruence when it's an equivalence on every hom-set, and it can be composed
from left and right. -/
class Congruence : Prop where
  /-- `r` is an equivalence on every hom-set. -/
  isEquiv : ∀ {X Y}, IsEquiv _ (@r X Y)
  /-- Precomposition with an arrow respects `r`. -/
  compLeft : ∀ {X Y Z} (f : X ⟶ Y) {g g' : Y ⟶ Z}, r g g' → r (f ≫ g) (f ≫ g')
  /-- Postcomposition with an arrow respects `r`. -/
  compRight : ∀ {X Y Z} {f f' : X ⟶ Y} (g : Y ⟶ Z), r f f' → r (f ≫ g) (f' ≫ g)
#align category_theory.congruence CategoryTheory.Congruence

• Ah, and something else: there seems to be a bit of a duplication in the code: originally, it was shown that the composite of "quotient, then the lift of a functor" is isomorphic to the original functor, but then I added code showing that the functors are actually equal. It would make sense to reuse the latter to prove the former, or even remove it. But I guess that's for after the port. Does it deserve a porting note?

[jcommelin]

In general equalities of functors can be quite taxing on the kernel. And mathematically it isn't a very well-behaved notion anyways. That's why we often only state isomorphisms.

[jcommelin]

isEquiv looks good to me.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style