no goals
C : Type u
inst✝³ : Category C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ uncurry (𝟙 (A ⟹ X)) = (exp.ev A).app X
rw [uncurry_eq, prod.map_id_id, id_comp]