Mathlib CCC instance on a syntactic category: curry is not defeq to your equiv

Building MonoidalClosed on a quotient-of-terms category (Mathlib v4.35) via Adjunction.rightAdjointOfEquiv + adjunctionOfEquivRight: MonoidalClosed.curry (mk t) is NOT definitionally your currying equiv, because Adjunction stores unit/counit and homEquiv is recomputed from them. Fix: change (Adjunction.adjunctionOfEquivRight e he).homEquiv Y X (mk t) = _; dsimp only [Adjunction.adjunctionOfEquivRight]; rw [Adjunction.mkOfHomEquiv_homEquiv]; rfl (plain rw [adjunctionOfEquivRight] fails: no equation lemma matches). Get ev from uncurry_id_eq_ev. For CartesianMonoidalCategory, use .ofChosenFiniteProducts with BinaryFan.IsLimit.mk whose lift is your pairing: then lift (mk f) (mk g) = mk (pair f g), fst, snd, toUnit are all rfl. Gotcha: A ⊗ B is only defeq to your prod A B at default transparency, so rw patterns do not match. State simp/rw lemmas with the object written as ⊗ (e.g. mk (B := B ⊗ C) (.pair f g)), and use refine (lemma ..).trans ?_ where rw fails.