  For building the free cartesian closed category, we extend simple type theory with the type 1 (unit type) and the product type \(A \times B\), for \(A, B\) types. The terms are extended by adding pairing operations and projections and a special element of type 1. As in Lambek and Scott 1986, one can then define a notion of typed conversions between terms, and show that this relation is decidable. One can then show (Lambek and Scott 1986) that the category with types as objects and as morphisms from \(A\) to \(B\) the set of closed terms of type \(A \rightarrow B\) (with conversion as equality) is the free cartesian closed category. This can be used to show that equality between arrows in this category is decidable.