Theorems · Inductive type · category theory

CategoryTheory.Lax.LaxTrans

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

If η is a lax 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 : app a ≫ G.map f ⟶ F.map f ≫ app b 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.Lax

Cited by

17 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory