Lean4
/-- For a `V`-category `C`, construct the opposite `V`-category structure on the type `Cᵒᵖ`
using the braiding in `V`. -/
instance opposite : EnrichedCategory V Cᵒᵖ
where
Hom y x := EnrichedCategory.Hom x.unop y.unop
id x := EnrichedCategory.id x.unop
comp z y x := (β_ _ _).hom ≫ EnrichedCategory.comp (x.unop) (y.unop) (z.unop)
id_comp _
_ :=
by
simp only [braiding_naturality_left_assoc, braiding_tensorUnit_left, Category.assoc, Iso.inv_hom_id_assoc]
exact EnrichedCategory.comp_id _ _
comp_id _
_ :=
by
simp only [braiding_naturality_right_assoc, braiding_tensorUnit_right, Category.assoc, Iso.inv_hom_id_assoc]
exact EnrichedCategory.id_comp _ _
assoc _ _ _
_ := by
simp only [braiding_naturality_left_assoc, MonoidalCategory.whiskerLeft_comp, Category.assoc]
rw [← EnrichedCategory.assoc]
simp only [braiding_tensor_left_hom, Category.assoc, Iso.inv_hom_id_assoc, braiding_naturality_right_assoc,
braiding_tensor_right_hom]
