Theorems · Inductive type · category theory

CategoryTheory.Oplax.OplaxTrans

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.OplaxFunctor B C → CategoryTheory.OplaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)

If η is an oplax transformation between F and G, we have a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. We also have a 2-morphism η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f for each 1-morphism f : a ⟶ b. These 2-morphisms satisfy the naturality condition, and preserve the identities and the compositions modulo some adjustments of domains and codomains of 2-morphisms.

Defined in

Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Cited by

24 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory