Theorems · Definition · category theory

CategoryTheory.Lax.LaxTrans.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} →
            {t : CategoryTheory.Lax.LaxTrans F G} →
              {B' : Type u₁} →
                {inst' : CategoryTheory.Bicategory B'} →
                  {C' : Type u₂} →
                    {inst'_1 : CategoryTheory.Bicategory C'} →
                      {F' G' : CategoryTheory.LaxFunctor B' C'} →
                        {t' : CategoryTheory.Lax.LaxTrans F' G'} →
                          B = B' →
                            inst ≍ inst' →
                              C = C' →
                                inst_1 ≍ inst'_1 →
                                  F ≍ F' → G ≍ G' → t ≍ t' → CategoryTheory.Lax.LaxTrans.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms