Commit 2023-03-02 07:41 591d4802

View on Github →

feat: port CategoryTheory.Category.Pairwise (#2534)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Category/Pairwise.lean

added inductive CategoryTheory.Pairwise.Hom

added def CategoryTheory.Pairwise.cocone

added def CategoryTheory.Pairwise.coconeIsColimit

added def CategoryTheory.Pairwise.coconeιApp

added def CategoryTheory.Pairwise.comp

added def CategoryTheory.Pairwise.diagram

added def CategoryTheory.Pairwise.diagramMap

added def CategoryTheory.Pairwise.diagramObj

added def CategoryTheory.Pairwise.id

added inductive CategoryTheory.Pairwise