Theorems · Inductive type · category theory

CategoryTheory.LaxFunctor

(B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A lax functor F between bicategories B and C consists of a function between objects F.obj, a function between 1-morphisms F.map, and a function between 2-morphisms F.map₂. Unlike functors between categories, F.map does not need to strictly commute with composition, and does not need to strictly preserve the identity. Instead, there are specified 2-morphisms 𝟙 (F.obj a) ⟶ F.map (𝟙 a) and F.map f ≫ F.map g ⟶ F.map (f ≫ g). F.map₂ strictly commutes with composition and preserves the identity. It also preserves the associator, the left unitor, and the right unitor modulo some adjustments of domains and codomains of 2-morphisms.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Lax

Cited by

201 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory