ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named IsArrowExponential refinement (#706) rather than the ad hoc IsExponential && IsArrow combination that lived here previously. More...

Concept definition

template<typename A>

concept dedekind::category::HasAxiom6Exponentiation = IsArrowExponential<Exponential<A, A>, A, A>

dedekind::category::HasAxiom6Exponentiation

ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named IsArrowExponential re...

Definition etcs.cppm:167

dedekind::category::IsArrowExponential

An exponential E : A → B that also satisfies the project's morphism vocabulary (IsArrow with matching...

Definition cartesian.cppm:178

Detailed Description

ETCS axiom 6 witness: exponentials B^A exist (here A^A witness). Uses the named IsArrowExponential refinement (#706) rather than the ad hoc IsExponential && IsArrow combination that lived here previously.