Exponential

Definition

Def Exponential
Let the category have binary products. An exponential of objects and consists of an object and an morphism such that, for any object and morphism there is a unique morphism such that And we call such evaluation, and the exponential transpose of .

Definition

Def Transpose
Given any morphism , the transpose of is given by

Proposition

Prop .

Prop .
Proof

Definition

Def Cartesian Closed
A category is called cartesian closed, if it has all finite products and exponentials.
e.g. We already have as one example, but note that also is cartesian closed, since for finite sets , the set of functions has cardinality .

Prop In cartesian closed category , we have for the terminal object .

Prop In any cartesian closed category , exponentiation by a fixed object defines a functor:
Prop In a cartesian closed category with coproducts, the products necessarily distribute over the coproducts:
Thrm In any cartesian closed category , there is always an isomorphism: for any -objects .

Thrm In any cartesian closed category , there is always an isomorphism: for any -objects .

Heyting Algebra

Def Heyting Algebra
A Heyting algebra is a poset with

1. Finite meets: and
2. Finite joins: and
3. Exponentials: for each , an element such that