instEnrichedCategoryTransportEnrichment

Lean4
instance : EnrichedCategory W (TransportEnrichment F C)
    where
  Hom := fun X Y : C => F.obj (X ⟶[V] Y)
  id := fun X : C => ε F ≫ F.map (eId V X)
  comp := fun X Y Z : C => μ F _ _ ≫ F.map (eComp V X Y Z)
  id_comp X
    Y :=
    by
    simp only [comp_whiskerRight, Category.assoc, Functor.LaxMonoidal.μ_natural_left_assoc,
      Functor.LaxMonoidal.left_unitality_inv_assoc]
    simp_rw [← F.map_comp]
    convert F.map_id _
    simp
  comp_id X
    Y :=
    by
    simp only [MonoidalCategory.whiskerLeft_comp, Category.assoc, Functor.LaxMonoidal.μ_natural_right_assoc,
      Functor.LaxMonoidal.right_unitality_inv_assoc]
    simp_rw [← F.map_comp]
    convert F.map_id _
    simp
  assoc P Q R
    S := by
    rw [comp_whiskerRight, Category.assoc, μ_natural_left_assoc, ← associativity_inv_assoc, ← F.map_comp, ← F.map_comp,
      e_assoc, F.map_comp, MonoidalCategory.whiskerLeft_comp, Category.assoc, Functor.LaxMonoidal.μ_natural_right_assoc]
Похожие утверждения