Structures · Category theory
CategoryTheory.Bicategory.Strict
A bicategory is called Strict if the left unitors, the right unitors, and the associators are
isomorphisms given by equalities.
- Shape
- One type argument · adds id_comp, comp_id, assoc, leftUnitor_eqToIso, rightUnitor_eqToIso, associator_eqToIso
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances8
- CategoryTheory.BasedCategory
- CategoryTheory.CatEnriched
- CategoryTheory.CatEnrichedOrdinary
- CategoryTheory.Cat
- CategoryTheory.LocallyDiscrete
- CategoryTheory.Bicategory.InducedBicategory
- SSet.QCat
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by96
- CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso
- CategoryTheory.StrictPseudofunctor.mk''
- CategoryTheory.Bicategory.Strict.associator_eqToIso
- CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso
- CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv
- CategoryTheory.Pseudofunctor.mapComp'_id_comp
- CategoryTheory.Bicategory.Strict.id_comp
- CategoryTheory.Pseudofunctor.mapComp'_comp_id
- CategoryTheory.Bicategory.Strict.comp_id
- CategoryTheory.Functor.toPseudofunctor'
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv
- CategoryTheory.Bicategory.Strict.assoc
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom
- CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom
- CategoryTheory.Pseudofunctor.isoMapOfCommSq
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_app
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom
- CategoryTheory.LaxFunctor.whiskerLeft_mapComp'_comp_mapComp'
- CategoryTheory.StrictPseudofunctor.toFunctor
- CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom
- CategoryTheory.Pseudofunctor.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight
- CategoryTheory.Pseudofunctor.isoMapOfCommSq_eq
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app_assoc
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_app
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_app
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom_app
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app
- CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'_assoc
- CategoryTheory.OplaxFunctor.mapComp'_comp_mapComp'_whiskerRight
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app
- CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp'
- CategoryTheory.LaxFunctor.mapComp'_whiskerRight_comp_mapComp'
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app
- CategoryTheory.Functor.toOplaxFunctor'
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app
- CategoryTheory.Pseudofunctor.mapComp'₀₁₃_inv_app
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app
- CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc
Ancestors0
No ancestors.