A category arrow equipped with explicit index cardinality metadata. More...

Concept definition

template<typename F>
concept dedekind::sequences::IsIndexedMorphismFamily =  IsArrow<F> && requires(const F f) {
  typename F::Domain;
  typename F::Codomain;
  typename F::cardinality_type;
  requires IsCardinality<typename F::cardinality_type>;
  { f.cardinality() } -> std::same_as<typename F::cardinality_type>;
}

Detailed Description

A category arrow equipped with explicit index cardinality metadata.

This concept captures families F: I -> X as first-class morphisms whose index species I and codomain species X are represented by Domain/Codomain, while cardinality metadata remains inspectable at compile time.