Theorems · Definition · category theory

CategoryTheory.Lax.LaxTrans.Modification.noConfusion

{P : Sort u} →
  {B : Type u₁} →
    {inst : CategoryTheory.Bicategory B} →
      {C : Type u₂} →
        {inst_1 : CategoryTheory.Bicategory C} →
          {F G : CategoryTheory.LaxFunctor B C} →
            {η θ : F ⟶ G} →
              {t : CategoryTheory.Lax.LaxTrans.Modification η θ} →
                {B' : Type u₁} →
                  {inst' : CategoryTheory.Bicategory B'} →
                    {C' : Type u₂} →
                      {inst'_1 : CategoryTheory.Bicategory C'} →
                        {F' G' : CategoryTheory.LaxFunctor B' C'} →
                          {η' θ' : F' ⟶ G'} →
                            {t' : CategoryTheory.Lax.LaxTrans.Modification η' θ'} →
                              B = B' →
                                inst ≍ inst' →
                                  C = C' →
                                    inst_1 ≍ inst'_1 →
                                      F ≍ F' →
                                        G ≍ G' →
                                          η ≍ η' →
                                            θ ≍ θ' →
                                              t ≍ t' → CategoryTheory.Lax.LaxTrans.Modification.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Bicategory.Modification.Lax

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound