instBicategory — Mathlib

Lean4
instance : Bicategory (CatEnrichedOrdinary C)
    where
  homCategory := inferInstance
  whiskerLeft {_ _ _} f {_ _} η := hComp (𝟙 f) η
  whiskerRight η h := hComp η (𝟙 h)
  associator f g h := eqToIso (assoc f g h)
  leftUnitor f := eqToIso (id_comp f)
  rightUnitor f := eqToIso (comp_id f)
  id_whiskerLeft := by simp [id_hComp]
  comp_whiskerLeft := by simp [← hComp_assoc]
  whiskerRight_id := by simp [hComp_id]
  whiskerRight_comp := by simp [hComp_assoc]
  whisker_assoc := by simp [hComp_assoc]
  pentagon := by simp [id_eq_eqToHom, -eqToHom_refl]
  triangle := by simp [id_eq_eqToHom, -eqToHom_refl]
Похожие утверждения