V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ ((𝟙 (𝟙_ V) ⊗ 𝟙 X.V) ≫ (λ_ X.V).hom) ≫ 𝟙 X.V = (λ_ X.V).hom
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ (λ_ X).hom.hom = (λ_ X.V).hom
dsimp [Monoidal.transport_leftUnitor]
no goals
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : MonCat
inst✝ : MonoidalCategory V
X : Action V G
⊢ ((𝟙 (𝟙_ V) ⊗ 𝟙 X.V) ≫ (λ_ X.V).hom) ≫ 𝟙 X.V = (λ_ X.V).hom
simp