Lean4
instance : MonoidalCategory (F C)
where
tensorObj X Y := FreeMonoidalCategory.tensor X Y
tensorHom := Quotient.map₂ Hom.tensor (fun _ _ hf _ _ hg ↦ HomEquiv.tensor hf hg)
whiskerLeft X _ _ f := Quot.map (fun f ↦ Hom.whiskerLeft X f) (fun f f' ↦ .whiskerLeft X f f') f
whiskerRight f Y := Quot.map (fun f ↦ Hom.whiskerRight f Y) (fun f f' ↦ .whiskerRight f f' Y) f
tensorHom_def
{W X Y Z} := by
rintro ⟨f⟩ ⟨g⟩
exact Quotient.sound (tensorHom_def _ _)
id_tensorHom_id _ _ := Quot.sound id_tensorHom_id
tensorHom_comp_tensorHom
{X₁ Y₁ Z₁ X₂ Y₂ Z₂} := by
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨g₁⟩ ⟨g₂⟩
exact Quotient.sound (tensorHom_comp_tensorHom _ _ _ _)
whiskerLeft_id X Y := Quot.sound (HomEquiv.whiskerLeft_id X Y)
id_whiskerRight X Y := Quot.sound (HomEquiv.id_whiskerRight X Y)
tensorUnit := FreeMonoidalCategory.unit
associator X Y Z := ⟨⟦Hom.α_hom X Y Z⟧, ⟦Hom.α_inv X Y Z⟧, Quotient.sound α_hom_inv, Quotient.sound α_inv_hom⟩
associator_naturality
{X₁ X₂ X₃ Y₁ Y₂ Y₃} := by
rintro ⟨f₁⟩ ⟨f₂⟩ ⟨f₃⟩
exact Quotient.sound (associator_naturality _ _ _)
leftUnitor X := ⟨⟦Hom.l_hom X⟧, ⟦Hom.l_inv X⟧, Quotient.sound l_hom_inv, Quotient.sound l_inv_hom⟩
leftUnitor_naturality
{X Y} := by
rintro ⟨f⟩
exact Quotient.sound (l_naturality _)
rightUnitor X := ⟨⟦Hom.ρ_hom X⟧, ⟦Hom.ρ_inv X⟧, Quotient.sound ρ_hom_inv, Quotient.sound ρ_inv_hom⟩
rightUnitor_naturality
{X Y} := by
rintro ⟨f⟩
exact Quotient.sound (ρ_naturality _)
pentagon _ _ _ _ := Quotient.sound pentagon
triangle _ _ := Quotient.sound triangle
