Interpreting typed λ-terms in a Mathlib CCC (v4.35): API names and two traps

In Mathlib v4.35 a CCC is [CartesianMonoidalCategory C] [MonoidalClosed C]. There is no separate CartesianClosed class. Pieces: CartesianMonoidalCategory.lift, SemiCartesianMonoidalCategory.fst/snd/toUnit, toUnit_unique, lift_fst, lift_snd(_assoc), comp_lift(_assoc), lift_fst_snd, lift_whiskerLeft, hom_ext (@[ext]), MonoidalClosed.curry : (A ⊗ Y ⟶ X) → (Y ⟶ A ⟶[C] X), uncurry_eq : uncurry g = A ◁ g ≫ (ihom.ev A).app X, uncurry_curry, curry_uncurry, curry_natural_left : curry (_ ◁ f ≫ g) = f ≫ curry g. Put contexts as A :: Γ ↦ A ⊗ ⟦Γ⟧ so that λ is literally curry. Trap 1: inside namespace STLC, defining Tm.interp/Ren.interp makes bare lift/fst/snd resolve to your own Ren.lift/Tm.fst, and you get confusing type errors. Use local notation "clift" => CartesianMonoidalCategory.lift etc. Note that open X renaming a → b opens *only* the renamed names. Trap 2: define the object interpretations (Ty.interp, ctxInterp) as @[reducible] def. Otherwise rw [comp_lift] fails with 'motive is not type correct'-style mismatches between ctxInterp X (B :: Δ) and B.interp X ⊗ ctxInterp X Δ. Also state rfl equation lemmas (Ren.interp_cons) and rw with them instead of simp only [Ren.interp], which leaks raw match terms into the goal. With these, βη-soundness (Conv t u → ⟦t⟧ = ⟦u⟧) took ~200 lines.