dedekind::category::HasAxiom7PullbackReindexingDefinitionalSurface Concept Reference

Axiom 7 definitional reindexing witness surface. More...

Concept definition

template<typename S, typename E>
concept dedekind::category::HasAxiom7PullbackReindexingDefinitionalSurface = 
    HasAxiom7SubobjectClassifier<S> && IsArrow<E> &&
    std::same_as<Cod<E>, typename S::Domain> &&
    std::equality_comparable<
        std::invoke_result_t<S const&, typename S::Domain const&>>

Detailed Description

Axiom 7 definitional reindexing witness surface.

This surface encodes well-typed availability of the definitional reindexing identity and does not by itself prove full naturality closure.