Theorems · Theorem · category theory

CategoryTheory.Oplax.OplaxTrans.mk.inj

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {app : (a : B) → F.obj a ⟶ G.obj a}
  {naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app b) ⟶ CategoryTheory.CategoryStruct.comp (app a) (G.map f)}
  {naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) (naturality g) =
          CategoryTheory.CategoryStruct.comp (naturality f) (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
      CategoryTheory.Oplax.OplaxTrans.naturality_naturality._autoParam}
  {naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a))
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
              (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
      CategoryTheory.Oplax.OplaxTrans.naturality_id._autoParam}
  {naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g))
            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
      CategoryTheory.Oplax.OplaxTrans.naturality_comp._autoParam}
  {app_1 : (a : B) → F.obj a ⟶ G.obj a}
  {naturality_1 :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app_1 b) ⟶ CategoryTheory.CategoryStruct.comp (app_1 a) (G.map f)}
  {naturality_naturality_1 :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app_1 b))
            (naturality_1 g) =
          CategoryTheory.CategoryStruct.comp (naturality_1 f)
            (CategoryTheory.Bicategory.whiskerLeft (app_1 a) (G.map₂ η)))
      CategoryTheory.Oplax.OplaxTrans.naturality_naturality._autoParam}
  {naturality_id_1 :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (naturality_1 (CategoryTheory.CategoryStruct.id a))
            (CategoryTheory.Bicategory.whiskerLeft (app_1 a) (G.mapId a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app_1 a))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app_1 a)).hom
              (CategoryTheory.Bicategory.rightUnitor (app_1 a)).inv))
      CategoryTheory.Oplax.OplaxTrans.naturality_id._autoParam}
  {naturality_comp_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (naturality_1 (CategoryTheory.CategoryStruct.comp f g))
            (CategoryTheory.Bicategory.whiskerLeft (app_1 a) (G.mapComp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app_1 c))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app_1 c)).hom
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality_1 g))
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.associator (F.map f) (app_1 b) (G.map g)).inv
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight (naturality_1 f) (G.map g))
                    (CategoryTheory.Bicategory.associator (app_1 a) (G.map f) (G.map g)).hom)))))
      CategoryTheory.Oplax.OplaxTrans.naturality_comp._autoParam},
  { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
      { app := app_1, naturality := naturality_1, naturality_naturality := naturality_naturality_1,
        naturality_id := naturality_id_1, naturality_comp := naturality_comp_1 } →
    app = app_1 ∧ naturality ≍ naturality_1

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms