Mathlib Map

Theorems · Definition · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.toLaxFunctor

{B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryLaxFunctor B C → CategoryTheory.LaxFunctor B C
Defined in
Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
Cited by
29 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
CategoryTheory.BicategoryCategoryTheory.Bicategory
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.StrictlyUnitaryLaxFunctor.comp · cited by 8StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.ext · cited by 4StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.mapIdIso · cited by 2StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.map_id · cited by 2StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map · cited by 0StrictlyUnitaryPseudofunc…CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapComp · cited by 0StrictlyUnitaryPseudofunc…CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_mapId · cited by 0StrictlyUnitaryPseudofunc…CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_map₂ · cited by 0StrictlyUnitaryPseudofunc…CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj · cited by 0StrictlyUnitaryPseudofunc…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_assoc · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_id · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapComp · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_mapId · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.StrictlyUnitaryLaxFunctor.comp_map₂ · cited by 0StrictlyUnitaryLaxFunctor…CategoryTheory.Bicategory · cited by 1587CategoryTheory.BicategoryCategoryTheory.LaxFunctor · cited by 201CategoryTheory.LaxFunctorCategoryTheory.StrictlyUnitaryLaxFunctor · cited by 17CategoryTheory.StrictlyUn…StrictlyUnitaryLaxFunctor.toL…CITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by31

Results whose statement or proof uses this declaration.