C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
⊢ (F.ε ≫ F.map (𝟙 (𝟙_ C)), G.ε ≫ G.map (𝟙 (𝟙_ C))) = (F.ε, G.ε)
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
⊢ (prod' F G).ε = (F.ε, G.ε)
dsimp [prod']
no goals
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category E
inst✝ : MonoidalCategory E
F : LaxMonoidalFunctor C D
G : LaxMonoidalFunctor C E
⊢ (F.ε ≫ F.map (𝟙 (𝟙_ C)), G.ε ≫ G.map (𝟙 (𝟙_ C))) = (F.ε, G.ε)
simp