Structures · Category theory
CategoryTheory.Functor.Braided
A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.
- Shape
- One type argument · adds braided
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances19
- CategoryTheory.Functor
- CategoryTheory.Over
- CategoryTheory.Discrete
- ModuleCat
- CategoryTheory.Grp
- Action
- CategoryTheory.Mon
- AddCommGrpCat
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.MonoidalOpposite
- CommGrpCat
- GrpCat
- AddGrpCat
- AlgCat
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
- QuadraticModuleCat
- CategoryTheory.Monoidal.Transported
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by56
- CategoryTheory.Functor.mapCommGrp
- CategoryTheory.Functor.mapCommGrpCompIso
- CategoryTheory.Equivalence.mapCommMon
- CategoryTheory.Functor.mapCommGrpNatTrans
- CategoryTheory.Functor.mapCommGrpNatIso
- CategoryTheory.Equivalence.mapCommGrp
- CategoryTheory.Adjunction.mapCommMon
- CategoryTheory.Adjunction.mapCommGrp
- CategoryTheory.Functor.map_braiding
- CategoryTheory.Functor.FullyFaithful.mapCommMon
- CategoryTheory.Functor.Braided.braided
- CategoryTheory.Functor.FullyFaithful.mapCommGrp
- CategoryTheory.Functor.instBraidedMonMapMon
- CategoryTheory.Functor.comp_mapCommGrp_one
- CategoryTheory.Functor.mapCommGrp_obj_grp_one
- CategoryTheory.Functor.Faithful.mapCommGrp
- CategoryTheory.Equivalence.mapCommGrp_inverse
- CategoryTheory.Functor.mapCommGrp_obj_X
- CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom
- CategoryTheory.Functor.Full.mapCommGrp
- CategoryTheory.Functor.Braided.toLaxBraided
- CategoryTheory.Functor.mapAddGrp.instMonoidal
- CategoryTheory.Functor.map_braiding_assoc
- CategoryTheory.Functor.instMonoidalMonMapAddMon
- CategoryTheory.Functor.mapCommGrp_obj_grp_mul
- CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom
- CategoryTheory.Pi.instBraidedForallPi'
- CategoryTheory.Equivalence.mapCommGrp_counitIso
- CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom
- CategoryTheory.Functor.Full.mapCommMon
- CategoryTheory.Equivalence.mapCommMon_unitIso
- CategoryTheory.Functor.instBraidedMonMapAddMon
- CategoryTheory.Functor.mapGrp.instBraided
- CategoryTheory.Functor.instMonoidalMonMapMon
- CategoryTheory.Adjunction.mapCommMon_counit
- CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom
- CategoryTheory.Equivalence.mapCommGrp_unitIso
- CategoryTheory.Functor.Braided.instComp
- CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage
- CategoryTheory.Adjunction.mapCommGrp_unit
- CategoryTheory.SymmetricCategory.ofFaithful
- CategoryTheory.Functor.mapAddGrp.instBraided
- CategoryTheory.Functor.mapGrp.instMonoidal
- CategoryTheory.Adjunction.mapCommGrp_counit
- CategoryTheory.Equivalence.mapCommMon_functor
- CategoryTheory.Equivalence.mapCommMon_inverse
- CategoryTheory.Pi.instBraidedForallPi
- CategoryTheory.Adjunction.mapCommMon_unit
- CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom
- CategoryTheory.Functor.mapCommGrp_obj_grp_inv