instBicategory — Mathlib

Lean4
instance : Bicategory (CatEnriched 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 := id_hComp
  comp_whiskerLeft := by simp [← id_hComp_id, hComp_assoc]
  whiskerRight_id := hComp_id
  whiskerRight_comp := by simp [hComp_assoc]
  whisker_assoc := by simp [hComp_assoc]
  pentagon f g h
    i := by
    generalize_proofs h1 h2 h3 h4; revert h1 h2 h3 h4
    generalize (f ≫ g) ≫ h = x, (g ≫ h) ≫ i = w
    rintro rfl _ rfl _; simp
  triangle f
    g := by
    generalize_proofs h1 h2 h3; revert h1 h2 h3
    generalize 𝟙 _ ≫ g = g, f ≫ 𝟙 _ = f
    rintro _ rfl rfl; simp
Похожие утверждения