Fact-checked by Grok 2 weeks ago

Exponential object

In category theory, an exponential object B^A in a category \mathcal{C} equipped with finite products is an object together with an evaluation morphism \mathrm{ev}_{A,B}: B^A \times A \to B satisfying the following universal property: for every object X in \mathcal{C} and every morphism f: X \times A \to B, there exists a unique morphism \hat{f}: X \to B^A—called the exponential transpose or curried form of f—such that the following diagram commutes:

\begin{CD} X \times A @>f>> B \\ @V{\hat{f} \times \mathrm{id}_A}VV @AA{\mathrm{ev}_{A,B}}A \\ B^A \times A @>{\mathrm{ev}_{A,B}}>> B \end{CD}

This property yields a natural isomorphism of hom-sets \mathcal{C}(X \times A, B) \cong \mathcal{C}(X, B^A), representing the functor -\times A \dashv (-)^A.^[1] Exponential objects generalize the notion of function spaces from set theory, enabling categories to internalize higher-order constructions such as currying, where a binary morphism is equivalently viewed as a unary morphism into an exponential.^[2] They are a defining feature of cartesian closed categories, which possess all finite products (including a terminal object) and, for every pair of objects A and B, an exponential object B^A.^[1] Such categories form the semantic foundation for typed lambda calculi and provide a categorical semantics for simply typed intuitionistic logic, where exponentials correspond to function types.^[3] In the category of sets \mathbf{Set}, the exponential object B^A is precisely the set of all functions from A to B, with evaluation given by function application (f, a) \mapsto f(a); this satisfies the universal property via currying, as any map X \times A \to B corresponds uniquely to a map X \to B^A sending each x \in X to the function a \mapsto f(x, a).^[2] Presheaf categories [\mathcal{D}^\mathrm{op}, \mathbf{Set}] are also cartesian closed, with exponentials computed pointwise: for presheaves F and G, the exponential G^F assigns to each object d \in \mathcal{D} the set of natural transformations F(-) \times \hom(-, d) \to G(-).^[3] In contrast, not all categories with products have exponentials; for instance, the category of Hausdorff topological spaces lacks them in general, though certain subcategories like compactly generated spaces do.^[4]

Background Concepts

Cartesian closed categories

A category \mathcal{C} is a mathematical structure consisting of a collection of objects and morphisms between them, satisfying axioms including composition of morphisms and identities, which formalize the notion of arrows transforming objects while preserving structure. Functors are mappings between categories that preserve their structure, sending objects to objects and morphisms to morphisms in a way compatible with composition and identities. Natural isomorphisms are special isomorphisms between functors that commute with the actions on morphisms in a coherent manner. A Cartesian closed category is a category \mathcal{C} equipped with finite products (including a terminal object) such that for every pair of objects A, B \in \mathcal{C}, the functor -\times A: \mathcal{C} \to \mathcal{C} admits a right adjoint, denoted [A, -] or (-)^A, yielding a natural isomorphism

\Hom_{\mathcal{C}}(X \times A, B) \cong \Hom_{\mathcal{C}}(X, B^A)

for all objects X, B \in \mathcal{C}.^[5] Here, B^A is the exponential object or internal hom-object representing morphisms from A to B "internalized" as an object within \mathcal{C}. The closure property of a Cartesian closed category refers to this internalization capability, where external function spaces (hom-sets) are represented by objects inside the category, enabling the category to model higher-order structures like function types without recourse to external constructions.^[5] The concept of closed categories was introduced by Samuel Eilenberg and G. M. Kelly in 1966.^[6] Cartesian closed categories were developed in the late 1960s as a special case using finite products. Dana Scott applied this framework around 1970 to domain theory, providing denotational semantics for the lambda calculus and addressing the need for categories that support recursive and higher-order computations.

Product and coproduct objects

In category theory, the product of two objects A and B in a category \mathcal{C}, denoted A \times B, is an object equipped with projection morphisms \pi_1: A \times B \to A and \pi_2: A \times B \to B.^[7] This structure satisfies the universal property: for any object C in \mathcal{C} and morphisms f: C \to A, g: C \to B, there exists a unique morphism h: C \to A \times B such that \pi_1 \circ h = f and \pi_2 \circ h = g.^[7] This property ensures that A \times B serves as the "most general" object from which both A and B can be reached simultaneously via the projections.^[8] Dually, the coproduct of A and B, often denoted A + B or A \coprod B, is an object equipped with injection morphisms \iota_1: A \to A + B and \iota_2: B \to A + B.^[9] It satisfies the dual universal property: for any object C and morphisms f: A \to C, g: B \to C, there exists a unique morphism h: A + B \to C such that h \circ \iota_1 = f and h \circ \iota_2 = g.^[9] This makes A + B the "least general" object into which both A and B can be injected.^[8] The terminal object, denoted $1, arises as the product over an empty family of objects; it is characterized by the existence of a unique morphism from any object to $1.^[7] Similarly, the initial object, denoted $0, is the coproduct over an empty family, with a unique morphism from $0 to any other object.^[9] In the category of sets (\mathbf{Set}), the product A \times B is the Cartesian product, with projections selecting the first and second components, while the coproduct A \coprod B is the disjoint union, where elements are tagged to distinguish origins.^[7] In the category of topological spaces (\mathbf{Top}), the product equips A \times B with the product topology (open sets as unions of products of opens), and the coproduct uses the disjoint union topology (open sets as disjoint unions of opens from each space).^[9] These constructions are prerequisites for categories with finite products, a requirement for Cartesian closed categories that support exponential objects.^[8]

Formal Definition

Universal property

In category theory, an exponential object B^A for objects A and B in a category \mathcal{C} equipped with finite products is defined by a representing object together with an evaluation morphism \mathrm{ev}_{A,B} \colon B^A \times A \to B that satisfies a universal mapping property.^[10] Specifically, for any object X in \mathcal{C} and any morphism f \colon X \times A \to B, there exists a unique morphism \hat{f} \colon X \to B^A such that the following diagram commutes:

\begin{CD} X \times A @>{\hat{f} \times \mathrm{id}_A}>> B^A \times A \\ @V{f}VV @VV{\mathrm{ev}_{A,B}}V \\ B @= B \end{CD}

This means \mathrm{ev}_{A,B} \circ (\hat{f} \times \mathrm{id}_A) = f.^[11] The morphism \hat{f} is often called the transpose or curry of f, capturing the essence of function abstraction in categorical terms.^[12] The universal property induces a natural isomorphism of functors \mathrm{Hom}_{\mathcal{C}}(-, B^A) \cong \mathrm{Hom}_{\mathcal{C}}(- \times A, B), where the left side varies over objects X. Under this isomorphism, the identity morphism on B^A corresponds to the evaluation map \mathrm{ev}_{A,B}.^[10] This bijection holds naturally in X, ensuring that exponential objects, when they exist, are unique up to unique isomorphism.^[11] A sketch of the isomorphism relies on the Yoneda lemma, which characterizes representable functors: the exponential B^A represents the contravariant functor \mathrm{Hom}_{\mathcal{C}}(- \times A, B) via the embedding of \mathcal{C} into its presheaf category.^[10] For existence, the category \mathcal{C} must possess all binary products, and the endofunctor - \times A must admit a right adjoint for each A; this holds in cartesian closed categories, which have all finite products (including a terminal object).^[11]

Equational characterization

The universal property of the exponential object in a cartesian closed category admits an equational characterization through the β- and η-rules, which capture the essential computational behavior of currying and evaluation morphisms. These rules derive directly from the adjunction underlying the closed structure and facilitate equational reasoning in proofs and term manipulations.^[13] Consider the evaluation morphism \mathrm{ev}_{A,B} \colon B^A \times A \to B. The β-rule states that for any morphism f \colon X \times A \to B, where \lambda f \colon X \to B^A denotes the curried form of f guaranteed by the universal property,

\mathrm{ev}_{A,B} \circ (\lambda f \times \mathrm{id}_A) = f.

This equation embodies the β-reduction, ensuring that applying a curried morphism recovers the original via evaluation.^[13] The η-rule provides the converse coherence: for any morphism g \colon A \to B^A,

\lambda (\mathrm{ev}_{A,B} \circ (g \times \mathrm{id}_A)) = g.

This rule enforces extensionality, identifying functions that agree on applications.^[13] In closed categories, these rules extend to equational axioms governing composition with evaluation, including associativity and unit laws. Specifically, there is an internal composition morphism \mathrm{comp}_{A,B,C} \colon C^B \times B^A \to C^A, the unique morphism such that

\mathrm{ev}_{A,C} \circ (\mathrm{comp}_{A,B,C} \times \mathrm{id}_A) = \mathrm{ev}_{B,C} \circ (\mathrm{id}_{C^B} \times \mathrm{ev}_{A,B}),

or equivalently, the curried form of \mathrm{ev}_{B,C} \circ (\mathrm{id}_{C^B} \times \mathrm{ev}_{A,B}) \colon C^B \times B^A \times A \to C. This satisfies associativity

\mathrm{comp}_{A,B,C} \circ (\mathrm{comp}_{A,B,D} \times \mathrm{id}_{D^C}) = \mathrm{comp}_{A,D,C} \circ (\mathrm{id}_{D^C} \times \mathrm{comp}_{B,D,C}),

along with unit laws such as \mathrm{comp}_{A,B,B} \circ (\eta_B \times \mathrm{id}_{B^A}) = \mathrm{id}_{B^A}, where \eta_B \colon B \to B^B is the unit of the adjunction (corresponding to the identity morphism via currying), and the dual for left units. These axioms, together with the β- and η-rules, form a sound equational basis for the closed structure.^[5] From these equations, the currying operation can be derived explicitly: given f \colon X \times A \to B, \lambda f is the unique solution to the β-equation, with uniqueness following from the η-rule and naturality. This equational approach underpins functional completeness, where the rules suffice to establish the full isomorphism of hom-sets without invoking the universal property ab initio.^[13]

Key Properties

Currying isomorphism

In a Cartesian closed category, the currying operation arises as a fundamental property of exponential objects, transforming a morphism f: A \times C \to B into a morphism \mathrm{curry}(f): A \to B^C. This currying map is defined via the universal property of the exponential object B^C, which comes equipped with an evaluation morphism \mathrm{ev}_{B,C}: B^C \times C \to B such that for any f: A \times C \to B, there exists a unique \mathrm{curry}(f): A \to B^C satisfying the equation \mathrm{ev}_{B,C} \circ (\mathrm{curry}(f) \times \mathrm{id}_C) = f.^[8] The inverse operation, uncurrying, maps a morphism g: A \to B^C back to \mathrm{uncurry}(g) = \mathrm{ev}_{B,C} \circ (g \times \mathrm{id}_C): A \times C \to B. These operations establish a natural isomorphism between the hom-sets \mathrm{Hom}(A \times C, B) \cong \mathrm{Hom}(A, B^C), natural in A, B, and C, thereby internalizing the abstraction of functions within the category.^[8] This bijection can be outlined through the universal property: given f: A \times C \to B, the uniqueness of \mathrm{curry}(f) ensures the mapping is well-defined and injective; surjectivity follows by applying the universal property to \mathrm{uncurry}(g) for any g: A \to B^C, yielding the inverse. The commutative diagram illustrating this is:

\begin{CD} A \times C @>f>> B \\ @V{\mathrm{curry}(f) \times \mathrm{id}_C}VV @AA{\mathrm{ev}_{B,C}}A \\ B^C \times C @>{\mathrm{ev}_{B,C}}>> B \end{CD}

confirming the equality via the evaluation map.^[8]^[14] The currying isomorphism implies contravariant functoriality for the exponential with respect to composition in the exponent: for morphisms g: D \to E and f: C \to D, the induced maps satisfy B^{g \circ f} \cong B^f \circ B^g: B^E \to B^C, preserving the structure of function spaces under relational composition.^[8]

Relation to adjunctions

In Cartesian closed categories, exponential objects arise naturally as part of an adjunction between the product functor and the exponential functor. For a fixed object A, the functor -\times A: \mathcal{C} \to \mathcal{C} is left adjoint to the functor (-) ^A: \mathcal{C} \to \mathcal{C}, where (-) ^A represents the exponential objects with codomain A. This adjunction is denoted -\times A \dashv (-) ^A. The unit of this adjunction is a natural transformation \eta: \mathrm{id}_\mathcal{C} \to (-) ^A \circ (-\times A), which for an object X provides a morphism \eta_X: X \to (X \times A)^A corresponding to the universal property of the exponential. The counit is a natural transformation \varepsilon: (-\times A) \circ (-) ^A \to \mathrm{id}_\mathcal{C}, where for objects B and A, the component \varepsilon_{B,A}: (B^A \times A) \to B is the evaluation morphism \mathrm{ev}_{B,A}, satisfying the triangular identities that characterize the adjunction. This perspective generalizes to the broader setting of closed categories equipped with a monoidal structure. In a monoidal category (\mathcal{C}, \otimes, I), the internal hom-object [-, -] (often denoted exponentially as (-)^\bullet) serves as the right adjoint to the tensor functor, satisfying - \otimes B \dashv [B , -] for fixed B, with the unit and counit defined analogously via currying and evaluation. Such categories are termed monoidal closed.^[8] Unlike Cartesian closed categories, where the monoidal structure is provided by the Cartesian product (which is both the categorical product and coproduct in the terminal object and preserves colimits), monoidal closed categories impose no such requirement on the tensor product \otimes. For instance, the category of modules over a commutative ring admits a closed monoidal structure under the tensor product of modules, but this tensor is not Cartesian. The foundational work on closed categories, including their relation to adjunctions via internal homs, was developed by Samuel Eilenberg and G. M. Kelly in the mid-1960s, providing the abstract framework that connects exponential objects to adjoint functors in non-Cartesian settings.^[6] This adjunction yields the currying isomorphism as a direct consequence, linking morphisms in product form to those in exponential form.

Examples

In the category of sets

In the category of sets, denoted \mathbf{Set}, the exponential object B^A for objects A and B is the set of all functions from A to B, often written as B^A = \{f \mid f: A \to B\}. The structure includes an evaluation morphism \mathrm{ev}: A \times B^A \to B defined by \mathrm{ev}(a, f) = f(a) for all a \in A and f \in B^A. This construction satisfies the universal property of the exponential object: for any set X and any morphism F: X \times A \to B, there exists a unique morphism g: X \to B^A such that the following diagram commutes,

\begin{tikzcd} X \times A \arrow[r, "F"] \arrow[d, "g \times \mathrm{id}_A"'] & B \\ B^A \times A \arrow[ur, "\mathrm{ev}"'] & \end{tikzcd}

or equivalently, \mathrm{ev} \circ (g \times \mathrm{id}_A) = F. The morphism g is defined pointwise by g(x)(a) = F(x, a) for all x \in X and a \in A, and its uniqueness follows from the fact that every function in B^A is determined by its values on elements of A. When A and B are finite sets with cardinalities |A| and |B|, respectively, the cardinality of the exponential object is |B^A| = |B|^{|A|}, reflecting the number of possible functions from a set of size |A| to one of size |B|.^[15] This exponential growth underscores the computational complexity of representing or enumerating function spaces in discrete settings. A notable special case arises when B = 2 = \{0, 1\}, the two-element set; here, $2^A is isomorphic to the power set \mathcal{P}(A), the set of all subsets of A. The isomorphism is given by characteristic functions: for each subset S \subseteq A, the corresponding function \chi_S: A \to 2 satisfies \chi_S(a) = 1 if a \in S and $0 otherwise, with the evaluation map preserving this correspondence. This identifies the power set operation as an instance of the exponential construction in \mathbf{Set}, highlighting its role in modeling subsets via binary choices.

In topological spaces

In the category of topological spaces, denoted Top, the exponential object B^A for objects A and B is constructed as the set C(A, B) of all continuous functions from A to B, equipped with the compact-open topology. This topology is generated by a subbasis consisting of subbasic open sets of the form V(K, U) = \{f \in C(A, B) \mid f(K) \subseteq U\}, where K is a compact subset of A and U is an open subset of B.^[16] The compact-open topology ensures that the evaluation map \mathrm{ev}_{A,B}: A \times B^A \to B, defined by \mathrm{ev}_{A,B}(a, f) = f(a), is continuous whenever A is core-compact (equivalently, locally compact if A is Hausdorff).^[16] However, the category Top is not cartesian closed because not every pair of objects admits an exponential object satisfying the universal property. Specifically, exponentials exist only when the domain A is core-compact; for non-core-compact A, no topology on C(A, B) makes the natural bijection \mathrm{Hom}(X \times A, B) \cong \mathrm{Hom}(X, C(A, B)) hold as a bijection of sets of continuous maps for all test objects X. For core-compact domains like the real line \mathbb{R}, the compact-open topology on C(\mathbb{R}, \mathbb{R}) does satisfy the universal property, providing a natural isomorphism \mathrm{Top}(X \times \mathbb{R}, \mathbb{R}) \cong \mathrm{Top}(X, C(\mathbb{R}, \mathbb{R})) for all X. A classic counterexample for non-existence involves non-core-compact spaces like the rational numbers \mathbb{Q} (with the subspace topology from \mathbb{R}), for which the compact-open topology on C(\mathbb{Q}, \mathbb{R}) does not satisfy the required bijection, as the transpose maps do not preserve continuity universally.^[16] To remedy these issues, researchers have identified cartesian closed subcategories of Top where exponentials exist for all objects. One such subcategory is the category of compactly generated Hausdorff spaces (often denoted CGHaus or the "convenient category" in algebraic topology), which includes all CW-complexes, manifolds, and Euclidean spaces. In this subcategory, the exponential B^A is again C(A, B) with the compact-open topology (or the equivalent k-ification to ensure compactness generation), and the evaluation map remains continuous, satisfying the cartesian closed structure. This framework preserves the essential features of Top while enabling the full power of cartesian closed categories for applications in homotopy theory and beyond.^[17]

In typed lambda calculi

In the simply typed lambda calculus, types act as objects in a category, while well-typed terms serve as morphisms between those types. The exponential object B^A is interpreted as the function type A \to B, consisting of all lambda abstractions of the form \lambda x : A . t, where t is a term of type B. This construction ensures that the category generated by the typed lambda calculus is Cartesian closed, with the product types corresponding to Cartesian products and the exponential providing the necessary closure under function spaces.^[18] The universal property of the exponential object manifests in the evaluation mechanism of the lambda calculus. Specifically, the evaluation morphism \mathrm{ev}_{A,B} : A \times B^A \to B corresponds to the application of a function term to an argument, governed by the β-reduction rule: if M = \lambda x : A . t : A \to B and N : A, then M \, N reduces to t[N/x], the body of M with x substituted by N. This reduction preserves typing and captures the computational content of function application in a typed setting.^[19] The Curry-Howard correspondence further links this structure to intuitionistic logic, where the exponential object B^A models the implication A \to B, lambda terms act as proofs inhabiting the type, and β-reduction reflects the logical rule of modus ponens. In this view, the simply typed lambda calculus provides a syntactic model for Cartesian closed categories, with proofs-as-programs establishing a deep isomorphism between logical deduction and typed computation.^[20] Such categories offer denotational semantics for typed lambda terms, interpreting types as domains and terms via hom-sets, with the currying isomorphism \hom(A \times B, C) \cong \hom(B, C^A) directly modeling lambda abstraction as a natural transformation. This semantic framework validates the equational theory of the lambda calculus, including β- and η-equality, ensuring soundness and adequacy of the interpretation.

Applications

In mathematical logic

In mathematical logic, exponential objects provide a categorical foundation for modeling implication in intuitionistic systems. Cartesian closed categories (CCCs), equipped with exponential objects, serve as models for the implicational fragment of intuitionistic propositional logic (with conjunction, implication, and truth), where the exponential B^A denotes the implication A \to B. The evaluation morphism \mathrm{ev}_{A,B} : B^A \times A \to B captures the modus ponens rule, enabling the composition of a proof of A \to B with a proof of A to produce a proof of B.^[21] Cartesian closed categories are sound and complete for the simply typed lambda calculus, which is equivalent to typed combinatory logic, linking the categorical structure of exponentials to the combinators for function abstraction and application in higher-order proof systems.^[22] This equivalence highlights how exponential objects encode the higher-order aspects of intuitionistic proofs, with typed combinatory terms corresponding to morphisms in the category. Higher exponentials, such as A \to (B \to C), model higher-order functions and implications in extensions of intuitionistic logic, allowing nested function spaces that represent quantification over proofs. These structures facilitate the semantics of higher-order logic by interpreting iterated implications as objects in the category.^[21] Full intuitionistic propositional logic requires additional structure beyond pure CCCs, such as coproducts to interpret disjunction and an initial object for falsehood. Classical propositional logic demands yet further structure to validate principles like the law of excluded middle and double negation elimination, such as in Boolean categories or Heyting algebras with additional axioms. Typed lambda calculi provide a syntactic counterpart to these categorical models, mirroring the proof-theoretic content of exponentials.^[22]

In computer science

In functional programming languages such as Haskell, exponential objects manifest as function types, where the type a \to b represents the exponential object b^a in the category Hask, with objects as Haskell types and morphisms as pure functions. This structure enables higher-order functions and partial application, as the currying isomorphism identifies functions of multiple arguments with functions returning functions, for instance, transforming a function of type (a, b) \to c into a \to b \to c. This categorical foundation underpins Haskell's type system, allowing seamless composition and abstraction in code.^[23] Exponential objects also appear in the context of monads and computational effects through Kleisli categories. For the IO monad, which models side effects like input/output, the Kleisli category has the same objects as Hask but morphisms as functions of type a \to \text{IO } b, with composition via the monadic bind operator \gg=; here, exponential objects correspond to effectful function types, enabling the sequencing of impure computations while preserving referential transparency. Similarly, the state monad, with type s \to (a, s), forms a Kleisli category where exponentials facilitate stateful transformations, such as updating internal state during function application, as explored in categorical models of effects.^[24]^[25] In domain theory, exponential objects provide the basis for denotational semantics of recursive programs. Scott domains, algebraic complete partial orders (cpos) with a least element and finite suprema, form a cartesian closed category under continuous functions, where the exponential D \to E is the domain of all continuous functions from D to E equipped with the pointwise order. This closure allows modeling recursive definitions via least fixed points, as in solving domain equations like D \cong [D \to D] for the denotations of recursive functions in languages with loops or fixed-point combinators, foundational to interpreting higher-order functional languages.^[26]^[27] Post-2000 developments in homotopy type theory (HoTT) leverage exponential objects for advanced type structures, particularly in representing paths and identities. In HoTT, function types A \to B serve as exponentials in the type-theoretic category, supporting dependent types and univalence; identity types \text{Id}_A(x, y), interpreted as path spaces, rely on this structure to model equivalences between types as paths in the type universe, enabling synthetic homotopy theory for verified software and mathematics. This integration, building on Martin-Löf type theory, has influenced proof assistants like Coq and Agda for formalizing computational properties with higher-dimensional paths.^[28]

References

[1]
https://arxiv.org/pdf/1612.09375.pdf#page=164
[2]
https://arxiv.org/pdf/1612.09375.pdf#page=48
[3]
https://arxiv.org/pdf/1612.09375.pdf#page=166
[4]
https://arxiv.org/pdf/1612.09375.pdf#page=167
[5]
cartesian closed category in nLab
### Summary of Cartesian Closed Category from nLab
[6]
Data Types as Lattices | SIAM Journal on Computing
Data Types as Lattices. Author: Dana ScottAuthors Info & Affiliations. https ... A Cartesian Closed Category of Domains with Almost Algebraic Bases.
[7]
https://ncatlab.org/nlab/show/product
[8]
Categories for the Working Mathematician - SpringerLink
Categories for the Working Mathematician provides an array of general ideas useful in a wide variety of fields. Starting from the foundations, this book ...
[9]
coproduct in nLab
Apr 10, 2025 · The notion of coproduct is a generalization to arbitrary categories of the notion of disjoint union in the category Set.
[10]
exponential object in nLab
### Summary of Exponential Objects in Category Theory
[11]
[PDF] Category Theory
So when they exist, exponential objects are unique up to (unique) isomorphism. exponentials of any pair of objects. This is a key concept for the semantics of ...
[12]
Exponentials, Currying, and Universal Constructions
Jun 17, 2014 · In general, a category in which there is a terminal object, a product of any two objects, and an exponential of any two objects is called ...
[13]
currying in nLab
Jan 7, 2023 · Currying is a process of transforming an operation on two variables into an operation on one variable that returns a function taking the second variable as an ...
[14]
[PDF] A Short Review of Cardinality - Christopher Heil
Jun 24, 2017 · We say that two sets A and B have the same cardinality if there exists a bijection f that maps A onto B, i.e., if there is a function f : A → B ...<|separator|>
[15]
[PDF] Topologies on spaces of continuous functions∗ - Martin Escardo
Topologies on spaces of continuous functions∗. Martın Escardó† and. Reinhold Heckmann‡. Version of 9th October 2001. Abstract. It is well-known that a Hausdorff ...
[16]
Monoidal closed, Cartesian closed and convenient categories ... - MSP
N. E. Steenrod, A convenient category of topological spaces, Michigan Math. J.,. 14 (1967), 133-152. 21. J. Tillotson, The convenient category of sequential ...
[17]
Cartesian closed categories and typed λ-calculi - SpringerLink
Jun 5, 2005 · J. Lambek, Functional completeness of cartesian categories, Ann. Math. Logic 6 (1974), 259–292. Google Scholar. J.
[18]
The Lambda Calculus - Stanford Encyclopedia of Philosophy
Dec 12, 2012 · $\beta$-reduction, or $\beta$-conversion, is the heart of the $\lambda$-calculus. When one actually applies $\beta$-reduction to reduce ...
[19]
[PDF] Lectures on the Curry Ho ard &somorphism
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational.
[20]
https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf
[21]
Locally cartesian closed categories and type theory
Oct 24, 2008 · It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed.
[22]
[PDF] What is a Categorical Model of Intuitionistic Linear Logic?
Seely's model arises from at least the desire to make the co-Kleisli category a cartesian closed category (CCC), which is achieved by including the n and p.
[23]
[PDF] The Equivalence of Typed λ Calculi and Cartesian Closed Categories
It turns out that typed λ calculi are structurally equivalent to a kind of category in category theory called the Cartesian closed cat- egory. This entails the ...
[24]
[PDF] Applied Category Theory Monads and Haskell - UChicago Math
Jun 20, 2022 · This is in itself a Haskell type. In other words, the Hask category has exponential objects. This is the first taste of categorical language in ...
[25]
[PDF] Notions of computation and monads
Kleisli triples are just an alternative description for monads. Although the formers are easy to justify from a computational perspective, the latters are more ...<|separator|>
[26]
[PDF] Monads and Adjunctions for Global Exceptions
(iii) Let T be a strong monad on C. • T has Kleisli exponentials when it is equipped, for every pair of C- objects A, B, with ...
[27]
[PDF] SEMANTIC DOMAINS - Illinois Security Lab
The theory of domains was established in order to have appropriate spaces on which to de ne semantic functions for the denotational approach to programming- ...
[28]
(PDF) Domains for Denotational Semantics. - ResearchGate
The purpose of the theory of domains is to give models for spaces on which to define computable functions. The kinds of spaces needed for denotational ...
[29]
[PDF] Homotopy Type Theory: Univalent Foundations of Mathematics
The present work has its origins in our collective attempts to develop a new style of “informal type theory” that can be read and understood by a human be- ing, ...<|control11|><|separator|>