Theorems · Definition · category theory

CategoryTheory.MorphismProperty.HasQuotient.casesOn

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {homRel : HomRel C} →
        [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel] →
          [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] →
            {motive : W.HasQuotient homRel → Sort u} →
              (t : W.HasQuotient homRel) →
                ((iff : ∀ ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄, homRel f g → (W f ↔ W g)) → motive ⋯) → motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Quotient

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.HomRel.IsStableUnderPrecompCategoryTheory.HomRel.IsStableUnderPostcomp