Theorems · Definition · category theory

CategoryTheory.StrictPseudofunctor.noConfusion

{P : Sort u} →
  {B : Type u₁} →
    {inst : CategoryTheory.Bicategory B} →
      {C : Type u₂} →
        {inst_1 : CategoryTheory.Bicategory C} →
          {t : CategoryTheory.StrictPseudofunctor B C} →
            {B' : Type u₁} →
              {inst' : CategoryTheory.Bicategory B'} →
                {C' : Type u₂} →
                  {inst'_1 : CategoryTheory.Bicategory C'} →
                    {t' : CategoryTheory.StrictPseudofunctor B' C'} →
                      B = B' →
                        inst ≍ inst' →
                          C = C' → inst_1 ≍ inst'_1 → t ≍ t' → CategoryTheory.StrictPseudofunctor.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext