dedekind::category::IsCartesianClosed Concept Reference

A Category equipped with Terminal Objects, Products, and Exponentials. More...

Concept definition

template<typename Cat>
concept dedekind::category::IsCartesianClosed = 
    IsCartesian<Cat> &&
    requires(typename Cat::Arrow::Domain A, typename Cat::Arrow::Codomain B) {
      
      
      
      
      typename Cat::template Exponential<decltype(A), decltype(B)>;
      requires IsExponential<
          typename Cat::template Exponential<decltype(A), decltype(B)>,
          decltype(A), decltype(B)>;
    }

Detailed Description

A Category equipped with Terminal Objects, Products, and Exponentials.

This concept extends IsSmallCategory to satisfy the three axioms of a Cartesian Closed Category (CCC):

1. Terminal Object — a unique sink 1 (represented by One / std::monostate).
2. Products — for any two objects A, B, a product A × B exists (represented by std::pair<A, B>).
3. Exponentials — for any two objects A, B, a function space B^A exists: an object whose inhabitants are functions A→B (IsExponential). B^A is an object, not an arrow; arrow-shaped carriers that also carry Domain/Codomain are a representation refinement (IsArrowExponential), used e.g. by Set<T>::Exponential's default — not required here.

This triple of structures provides the categorical foundations required for the Dedekind topos (ETCS).