Theorems · Inductive type · category theory

CategoryTheory.Lax.StrongTrans

{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₂)

A strong natural transformation between lax functors F and G is a natural transformation that is "natural up to 2-isomorphisms". More precisely, it consists of the following: * a 1-morphism η.app a : F.obj a ⟶ G.obj a for each object a : B. * a 2-isomorphism η.naturality f : app a ≫ G.map f ≅ F.map f ≫ app b for each 1-morphism f : a ⟶ b. * These 2-isomorphisms 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

16 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory