Theorems · Definition · category theory

CategoryTheory.EffectiveEquivalenceRelation.mk.noConfusion

{C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {R A : C} →
      {p₁ p₂ : R ⟶ A} →
        {P : Sort u} →
          {toEquivalenceRelation : CategoryTheory.EquivalenceRelation p₁ p₂} →
            {B : C} →
              {π : A ⟶ B} →
                {isKernelPair : CategoryTheory.IsKernelPair π p₁ p₂} →
                  {isPushout : CategoryTheory.IsPushout p₁ p₂ π π} →
                    {toEquivalenceRelation' : CategoryTheory.EquivalenceRelation p₁ p₂} →
                      {B' : C} →
                        {π' : A ⟶ B'} →
                          {isKernelPair' : CategoryTheory.IsKernelPair π' p₁ p₂} →
                            {isPushout' : CategoryTheory.IsPushout p₁ p₂ π' π'} →
                              { toEquivalenceRelation := toEquivalenceRelation, B := B, π := π,
                                    isKernelPair := isKernelPair, isPushout := isPushout } =
                                  { toEquivalenceRelation := toEquivalenceRelation', B := B', π := π',
                                    isKernelPair := isKernelPair', isPushout := isPushout' } →
                                (toEquivalenceRelation ≍ toEquivalenceRelation' → B ≍ B' → π ≍ π' → P) → P

Defined in

Mathlib.CategoryTheory.EquivalenceRelation

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms