Normalisation of the Theory T of Cartesian Closed Categories and Conservativity of Extensions T[x] of T
LIRMM, 161 rue ADA, 34392 Montpellier, France; email@example.com.
2 LIRMM, 161 rue ADA, 34392 Montpellier, France; firstname.lastname@example.org.
Accepted: March 1999
Using an inductive definition of normal terms of the theory of Cartesian Closed Categories with a given graph of distinguished morphisms, we give a reduction free proof of the decidability of this theory. This inductive definition enables us to show via functional completeness that extensions of such a theory by new constants (“indeterminates”) are conservative.
Mathematics Subject Classification: 03F05 / 03B25 / 18D15
© EDP Sciences, 1999