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