⟨f, g⟩ : A → B × C, one argument into a product. More...
Public Types | |
| using | Domain = Dom<F> |
| using | Codomain = std::pair<Cod<F>, Cod<G>> |
Public Member Functions | |
| constexpr Codomain | operator() (const Domain &x) const |
Public Attributes | |
| F | f |
| G | g |
Detailed Description
requires std::same_as<Dom<F>, Dom<G>>
struct dedekind::category::Pairing< F, G >
⟨f, g⟩ : A → B × C, one argument into a product.
cartesian__The_Formers_Of_Functions
Products and sums of functions: the algebraic data types of the posture, std::pair the product and std::variant the sum. Two formers are primitive: the pairing ⟨f, g⟩ sends one argument into a product, the copairing [f, g] is case analysis out of a sum (std::visit's shape: the fold of a sum). The other two are defined by them, as in the textbook: f × g = ⟨f ∘ π₁, g ∘ π₂⟩ and f + g = [ι₁ ∘ f, ι₂ ∘ g].
The law engine (:posetal, arrow_node) keeps × and + as facts of their own because the derived form loses precision: ⟨f ∘ π₁, g ∘ π₂⟩ is jointly injective though neither leg is, so the pairing rule alone certifies nothing. The readers below, and LawAlgebra's steer, recognise the defining form and apply the product (sum) fact to f and g; any other pairing gets the pairing rule, which is the honest answer (⟨f ∘ π₁, f ∘ π₁⟩ is not injective). Monotonicity is read on a product under the product order ProductLeq; a sum has no canonical order, so its variance stays at the engine's value level.
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/cartesian.cppm
