Structures · Category theory
CategoryTheory.Functor.LaxMonoidal
A functor F : C ⥤ D between monoidal categories is lax monoidal if it is
equipped with morphisms ε : 𝟙_ D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y),
satisfying the appropriate coherences.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Functor
- Shape
- One type argument · adds ε, μ, μ_natural_left, μ_natural_right, associativity, left_unitality, right_unitality
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances8
- CategoryTheory.Functor
- CategoryTheory.Discrete
- ModuleCat
- Action
- CategoryTheory.Mon
- CategoryTheory.Skeleton
- CategoryTheory.AddMon
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by176
- CategoryTheory.Functor.LaxMonoidal.μ
- CategoryTheory.Functor.LaxMonoidal.ε
- CategoryTheory.Functor.mapMon
- CategoryTheory.Functor.mapAddMon
- CategoryTheory.Functor.monObjObj
- CategoryTheory.Functor.addMonObjObj
- CategoryTheory.TransportEnrichment
- CategoryTheory.LaxMonoidalFunctor.of
- CategoryTheory.Functor.LaxMonoidal.μ_natural_right
- CategoryTheory.Functor.LaxMonoidal.right_unitality
- CategoryTheory.Functor.LaxMonoidal.associativity_assoc
- CategoryTheory.Functor.mapAddMonCompIso
- CategoryTheory.Functor.mapMonCompIso
- CategoryTheory.Functor.LaxMonoidal.left_unitality
- CategoryTheory.Functor.LaxMonoidal.μ_natural_left
- CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor
- CategoryTheory.Functor.mapMonNatIso
- CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse
- CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
- CategoryTheory.Functor.LaxMonoidal.associativity
- CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv
- CategoryTheory.Adjunction.unit_app_unit_comp_map_η
- CategoryTheory.Functor.mapMonNatTrans
- CategoryTheory.Functor.mapAddMonNatIso
- CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc
- CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
- CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc
- CategoryTheory.Functor.LaxMonoidal.μ_natural
- CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
- CategoryTheory.Functor.mapAddMonNatTrans
- CategoryTheory.μ_naturality₂
- CategoryTheory.Functor.LaxMonoidal.associativity_inv
- CategoryTheory.Functor.LaxMonoidal.left_unitality_inv
- CategoryTheory.Functor.LaxMonoidal.right_unitality_inv
- CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ
- CategoryTheory.Adjunction.mapMon
- CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ
- CategoryTheory.Adjunction.leftAdjointOplaxMonoidal
- CategoryTheory.Adjunction.mapAddMon
- CategoryTheory.ε_naturality_assoc
- CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ_assoc
- CategoryTheory.associativity_app
- CategoryTheory.Functor.LaxMonoidal.right_unitality_inv_assoc
- CategoryTheory.left_unitality_app
- CategoryTheory.Functor.LaxMonoidal.tensorHom_ε_comp_μ
- CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom
- CategoryTheory.Functor.obj.μ_def
- CategoryTheory.associativity_app_assoc
- CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ_assoc
- CategoryTheory.Functor.LaxMonoidal.ε_tensorHom_comp_μ
Ancestors0
No ancestors.