November 2017
Intermediate to advanced
670 pages
17h 35m
English
A cartesian closed category, where a product exists for any two elements and an exponential exists for any two elements, is a model for logic and type theory.
Though many categories have products and sums, only a few have map objects. Such categories are called cartesian closed categories.
There is a deep connection between λ-calculus, logic, and cartesian closed categories.
A cartesian closed category (CCC) is an abstraction having a small vocabulary with associated laws:
The category part means we have a notion of morphisms each having a domain and codomain object. There is an identity morphism for and associative composition operator.
The cartesian part means that we have products, with projection functions ...
Read now
Unlock full access