Browsing by Subject "category theory"
Now showing 1 - 1 of 1
- Results Per Page
- Sort Options
Item Cartesian Closed Categories and Typed Lambda Calculi(2016) Menezes, Dean; Blumberg, AndrewTyped lambda categories and Cartesian closed categories are both means of formalizing the process of substitution; we demonstrate that these views are essentially the same; specifically that there is an equivalence between the category of small Cartesian closed categories and the category of typed lambda calculi. First we introduce the basic notions of category, functor, monad, comonad and equivalence of categories; then we use these notions to define the category of small Cartesian closed categories and describe how additional arrows may be adjoined to a Cartesian closed category. Next we provide a definition of a typed lambda calculus and describe the structure-preserving maps or translations between typed lambda calculi. Next we provide a definition of a typed lambda calculus and describe the structure-preserving maps or translations between typed lambda calculi. Having defined the two categories we provide descriptions of functors L : Cart_N to lambda-calc and C: lambda-calc to Cart_N and then show that the functors give an equivalence of categories.