dedekind::category::IsGrothendieckTopology Concept Reference

Signature-level witness for Grothendieck coverage rules over sieves. More...

Concept definition

template<typename J, typename S>
concept dedekind::category::IsGrothendieckTopology = 
    IsSieve<S> && requires(S s, typename S::Arrow f) {
      { J::is_cover(s) } -> std::convertible_to<bool>;
      { J::identity_cover(s.target()) } -> std::convertible_to<bool>;
      { J::is_cover(s.pullback_along(f)) } -> std::convertible_to<bool>;
      { J::pullback_stable(s, f) } -> std::convertible_to<bool>;
      { J::transitive(s) } -> std::convertible_to<bool>;
    }

Detailed Description

Signature-level witness for Grothendieck coverage rules over sieves.

This concept encodes the three textbook shape obligations used by this project's ETCS narrative:

1. Identity cover witness,
2. Pullback-stability witness,
3. Transitivity witness.

It is a proof-surface contract: implementations may use stronger internal laws, but these witnesses keep API-level claims reviewable and testable.