I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories. What's the internal language of the opposite type of category? The rules dual to currying and uncurrying are: $$ \mathrm{mal} : \mathrm{Hom}(b, a + c) \to \mathrm{Hom}(b \vdash a, c) \\ \ma...