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

A projection morphism π : E -> B for a bundle candidate. More...

Concept definition

template<typename Pi, typename E, typename B>
concept dedekind::category::IsBundleProjection =
IsArrow<Pi> && std::same_as<Dom<Pi>, E> && std::same_as<Cod<Pi>, B>
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::IsBundleProjection
A projection morphism π : E -> B for a bundle candidate.
Definition topoi.cppm:229

Detailed Description

A projection morphism π : E -> B for a bundle candidate.

This is a structural contract for the projection map in a fiber bundle. It keeps the proof surface explicit without forcing a concrete atlas model yet.