Theorems · Definition · category theory

CategoryTheory.Lax.LaxTrans.Modification.noConfusionType

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} →
              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'} → CategoryTheory.Lax.LaxTrans.Modification η' θ' → Sort u

Defined in

Mathlib.CategoryTheory.Bicategory.Modification.Lax

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.Bicategory