Lean4
/-- Formal compositions and tensor products of identities, unitors and associators. The morphisms
of the free monoidal category are obtained as a quotient of these formal morphisms by the
relations defining a monoidal category. -/
inductive Hom : F C → F C → Type u
| id (X) : Hom X X
| α_hom (X Y Z : F C) : Hom ((X.tensor Y).tensor Z) (X.tensor (Y.tensor Z))
| α_inv (X Y Z : F C) : Hom (X.tensor (Y.tensor Z)) ((X.tensor Y).tensor Z)
| l_hom (X) : Hom (unit.tensor X) X
| l_inv (X) : Hom X (unit.tensor X)
| ρ_hom (X : F C) : Hom (X.tensor unit) X
| ρ_inv (X : F C) : Hom X (X.tensor unit)
| comp {X Y Z} (f : Hom X Y) (g : Hom Y Z) : Hom X Z
| whiskerLeft (X : F C) {Y₁ Y₂} (f : Hom Y₁ Y₂) : Hom (X.tensor Y₁) (X.tensor Y₂)
| whiskerRight {X₁ X₂} (f : Hom X₁ X₂) (Y : F C) : Hom (X₁.tensor Y) (X₂.tensor Y)
| tensor {W X Y Z} (f : Hom W Y) (g : Hom X Z) : Hom (W.tensor X) (Y.tensor Z)
