A small category equipped with a terminal object 1 and binary products × — a "cartesian category" in the textbook sense (Pierce, Basic Category Theory for Computer Scientists §1.4; Awodey). More...

Concept definition

template<typename Cat>
concept dedekind::category::IsCartesian =  IsSmallCategory<Cat> && requires {
  
  typename Cat::Terminal;
  requires IsTerminalObject<typename Cat::Terminal>;
} && requires(typename Cat::Arrow::Domain A, typename Cat::Arrow::Codomain B) {
  
  typename Cat::template Product<decltype(A), decltype(B)>;
  requires IsProduct<typename Cat::template Product<decltype(A), decltype(B)>,
                     decltype(A), decltype(B)>;
}

Detailed Description

A small category equipped with a terminal object 1 and binary products × — a "cartesian category" in the textbook sense (Pierce, Basic Category Theory for Computer Scientists §1.4; Awodey).

Concept-as-predicate framing: IsCartesian narrows the type-class IsSmallCategory by intersecting with the finite-product structure (terminal + binary products). This is the finite-products subset of finite limits — finitely complete categories also have equalisers and pullbacks, which are not pinned here; IsCartesian deliberately stops at the products-and-terminal layer.

Position in the size-and-structure lattice (read top-down as narrowing intersections; cf. paper §2.3):

IsSmallCategory<Cat>
  ∧ has terminal object @c Cat::Terminal
  ∧ has binary product @c Cat::template Product<A, B>
= IsCartesian<Cat>

The CCC-completing exponentials live downstream in :cartesian; IsCartesianClosed = IsCartesian + has-exponentials. Re-using IsCartesian as the prerequisite gates IsCartesianClosed cleanly against the chain IsSmallCategory → IsCartesian → IsCartesianClosed.