Two noob questions

Stream: new members

[debord]

Hello. Here's an MWE of the project I've gotten to start:

import Mathlib.CategoryTheory.Products.Basic

open CategoryTheory

namespace Quantum

universe v₁ v₂ u₁ u₂

variable (𝒞 : Type u₁) [Category.{v₁} 𝒞]

class MonoidalCategoryData where
  tensorProduct : 𝒞 × 𝒞 ⥤ 𝒞
  unitObject : 𝒞
  associator : ∀ A B C : 𝒞, tensorProduct.obj ((tensorProduct.obj (A, B)), C) ≅ tensorProduct.obj (A, (tensorProduct.obj (B, C)))
  leftUnitor : ∀ A : 𝒞, tensorProduct.obj (unitObject, A) ≅ A
  rightUnitor : ∀ A : 𝒞, tensorProduct.obj (A, unitObject) ≅ A

scoped notation:70 lhs:71 "⊗" rhs:70 => MonoidalCategoryData.tensorProduct.obj (lhs, rhs)
scoped notation:70 lhs:71 "⊕" rhs:70 => MonoidalCategoryData.tensorProduct.map (lhs, rhs)
scoped notation "𝕀" => MonoidalCategoryData.unitObject
scoped notation "α" => MonoidalCategoryData.associator
scoped notation "γ" => MonoidalCategoryData.leftUnitor
scoped notation "ρ" => MonoidalCategoryData.rightUnitor

class MonoidalCategory extends MonoidalCategoryData 𝒞 where
  triangle : ∀ A B : 𝒞, (α A 𝕀 B).hom ≫ ((𝟙 A) ⊕ (γ B).hom) = ((ρ A).hom ⊕ (𝟙 B) : (A ⊗ 𝕀) ⊗ B ⟶ A ⊗ B)
  pentagon : ∀ A B C D : 𝒞, ((α A B C).hom ⊕ (𝟙 D)) ≫ (α A (B ⊗ C) D).hom ≫ ((𝟙 A) ⊕ (α B C D).hom) = (α (A ⊗ B) C D).hom ≫ (α A B (C ⊗ D)).hom

variable (ℳ : Type u₂) [Category.{v₂} ℳ] [MonoidalCategory ℳ]

def State (A : ℳ) := 𝕀 ⟶ A

class WellPointedMonoidalCategory extends MonoidalCategory ℳ where
  wellpointed : ∀ A B : ℳ, ∀ f g : A ⟶ B, ∀ a : State A, a ≫ f = a ≫ g → f = g

Question 1: Why is State A on WellPointedMonoidalCategory giving a type mismatch error? Don't I define State as taking an input of type ℳ and I'm giving it an input of type ℳ?

Question 2: I want to define a notion of monoidally well pointed monoidal category. This goes like: for all pairs of morphisms $f,g : A_1 \otimes \cdots \otimes A_n \to B$ and all states $a_1 : I \to A_1, \ldots, a_n : I \to A_n$ bla bla... How do I express having an arbitrary n amount of tensor products or n states like that in Lean?