Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::HasAxiom1Composition Concept Referenceexport
module dedekind.category

ETCS axiom 1 witness: composition is available for ambient arrows. More...

Concept definition

template<typename A>
concept dedekind::category::HasAxiom1Composition =
IsArrow<Identity<A>> && IsArrow<decltype(id<A>() >> id<A>())>
dedekind::category::HasAxiom1Composition
ETCS axiom 1 witness: composition is available for ambient arrows.
Definition etcs.cppm:137
dedekind::category::IsArrow
A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain'...
Definition morphism.cppm:168
dedekind::category::id
constexpr auto id()
The Identity Factory: Returns the neutral arrow for Species A.
Definition morphism.cppm:634

Detailed Description

ETCS axiom 1 witness: composition is available for ambient arrows.