Structures · Category theory
CategoryTheory.Functor.LaxBraided
A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.
- Shape
- One type argument · adds braided
Extends1
Extended by1
Concrete types that are instances3
- CategoryTheory.Discrete
- CategoryTheory.Mon
- CategoryTheory.AddMon
How is a type an instance?
Loading the hierarchy index…
Assumed by39
- CategoryTheory.Functor.mapCommMon
- CategoryTheory.Functor.mapCommMonCompIso
- CategoryTheory.Functor.mapCommMonNatIso
- CategoryTheory.Functor.mapCommMonNatTrans
- CategoryTheory.LaxBraidedFunctor.of
- CategoryTheory.Functor.LaxBraided.braided
- CategoryTheory.Adjunction.mapCommMon
- CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ
- CategoryTheory.Functor.mapCommMon_obj_mon_mul
- CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom
- CategoryTheory.Functor.comp_mapCommMon_one
- CategoryTheory.Pi.instLaxBraidedForallPi
- CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom
- CategoryTheory.Pi.instLaxBraidedForallPi'
- CategoryTheory.Functor.instLaxBraidedMonMapAddMon
- CategoryTheory.Functor.comp_mapCommMon_mul
- CategoryTheory.Functor.mapCommMon_obj_X
- CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
- CategoryTheory.Functor.isCommMonObj_obj
- CategoryTheory.Functor.LaxBraided.toLaxMonoidal
- CategoryTheory.Functor.mapCommMon_map_hom_hom
- CategoryTheory.Functor.instIsMonHomμ
- CategoryTheory.Adjunction.mapCommMon_counit
- CategoryTheory.Functor.mapCommMon_obj_mon_one
- CategoryTheory.Functor.mapCommMonNatIso.congr_simp
- CategoryTheory.Functor.LaxBraided.ofNatIso
- CategoryTheory.Functor.LaxBraided.instComp
- CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ_assoc
- CategoryTheory.LaxBraidedFunctor.of_toFunctor
- CategoryTheory.Functor.mapCommMonNatTrans.congr_simp
- CategoryTheory.Functor.LaxBraided.braided_assoc
- CategoryTheory.Functor.Faithful.mapCommMon
- CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom
- CategoryTheory.Adjunction.mapCommMon_unit
- CategoryTheory.Functor.instLaxMonoidalMonMapMon
- CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom
- CategoryTheory.Functor.instIsAddMonHomμ
- CategoryTheory.Functor.instLaxMonoidalMonMapAddMon
- CategoryTheory.Functor.instLaxBraidedMonMapMon