Theorems · Definition · category theory

CategoryTheory.Lax.StrongTrans.mk.noConfusion

{B : Type u₁} →
  {inst : CategoryTheory.Bicategory B} →
    {C : Type u₂} →
      {inst_1 : CategoryTheory.Bicategory C} →
        {F G : CategoryTheory.LaxFunctor B C} →
          {P : Sort u} →
            {app : (a : B) → F.obj a ⟶ G.obj a} →
              {naturality :
                  {a b : B} →
                    (f : a ⟶ b) →
                      CategoryTheory.CategoryStruct.comp (app a) (G.map f) ≅
                        CategoryTheory.CategoryStruct.comp (F.map f) (app b)} →
                {naturality_naturality :
                    autoParam
                      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                        CategoryTheory.CategoryStruct.comp (naturality f).hom
                            (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η))
                            (naturality g).hom)
                      CategoryTheory.Lax.StrongTrans.naturality_naturality._autoParam} →
                  {naturality_id :
                      autoParam
                        (∀ (a : B),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
                              (naturality (CategoryTheory.CategoryStruct.id a)).hom =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).inv
                                (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))))
                        CategoryTheory.Lax.StrongTrans.naturality_id._autoParam} →
                    {naturality_comp :
                        autoParam
                          (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
                                (naturality (CategoryTheory.CategoryStruct.comp f g)).hom =
                              CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                                    (CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                                      (CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv
                                        (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)))))))
                          CategoryTheory.Lax.StrongTrans.naturality_comp._autoParam} →
                      {app' : (a : B) → F.obj a ⟶ G.obj a} →
                        {naturality' :
                            {a b : B} →
                              (f : a ⟶ b) →
                                CategoryTheory.CategoryStruct.comp (app' a) (G.map f) ≅
                                  CategoryTheory.CategoryStruct.comp (F.map f) (app' b)} →
                          {naturality_naturality' :
                              autoParam
                                (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                                  CategoryTheory.CategoryStruct.comp (naturality' f).hom
                                      (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app' b)) =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.Bicategory.whiskerLeft (app' a) (G.map₂ η)) (naturality' g).hom)
                                CategoryTheory.Lax.StrongTrans.naturality_naturality._autoParam} →
                            {naturality_id' :
                                autoParam
                                  (∀ (a : B),
                                    CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.whiskerLeft (app' a) (G.mapId a))
                                        (naturality' (CategoryTheory.CategoryStruct.id a)).hom =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.Bicategory.rightUnitor (app' a)).hom
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Bicategory.leftUnitor (app' a)).inv
                                          (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app' a))))
                                  CategoryTheory.Lax.StrongTrans.naturality_id._autoParam} →
                              {naturality_comp' :
                                  autoParam
                                    (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                                      CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Bicategory.whiskerLeft (app' a) (G.mapComp f g))
                                          (naturality' (CategoryTheory.CategoryStruct.comp f g)).hom =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.Bicategory.associator (app' a) (G.map f) (G.map g)).inv
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.Bicategory.whiskerRight (naturality' f).hom (G.map g))
                                            (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.Bicategory.associator (F.map f) (app' b) (G.map g)).hom
                                              (CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality' g).hom)
                                                (CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.Bicategory.associator (F.map f) (F.map g)
                                                      (app' c)).inv
                                                  (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app' c)))))))
                                    CategoryTheory.Lax.StrongTrans.naturality_comp._autoParam} →
                                { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
                                      naturality_id := naturality_id, naturality_comp := naturality_comp } =
                                    { app := app', naturality := naturality',
                                      naturality_naturality := naturality_naturality', naturality_id := naturality_id',
                                      naturality_comp := naturality_comp' } →
                                  (app ≍ app' → naturality ≍ naturality' → P) → P

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms