pullback.cppm File Reference

Limits — Equalizers and Fiber Products (Pullbacks). More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.category:limit;

Include dependency graph for pullback.cppm:

Classes
struct	dedekind::category::SubobjectInclusion< S >
	inclusion_arrow(S): the inclusion \(\iota_S : S \hookrightarrow \mathrm{Domain}(S)\) of a subobject as an arrow (Domain = S::Member, Codomain = S::Domain, through S's own ι), so it can be a leg of a cospan. A monomorphism by definition. More...
struct	dedekind::category::PullbackApex< Apex, A, B >
	The pullback apex of a meet of A and B: the apex itself, viewed with the subobject surface and the projection legs π_1 / π_2 (IsPullback). More...
struct	dedekind::category::PullbackApex< Apex, A, B >::Member
	A member of the apex: one value, read in each operand. Its components are the legs, Π<1, Member> and Π<2, Member> as arrows (:limit's projections), the co-restrictions A ∧ B ↪ A and A ∧ B ↪ B: inclusions, so monic, not epic. More...
struct	dedekind::category::PushoutApex< Apex, A, B >
	The pushout apex of a join of A and B: the apex viewed with the subobject surface and the coprojections ι1 / ι2 (IsPushout). Dual of PullbackApex. More...
struct	dedekind::category::PushoutApex< Apex, A, B >::Member
struct	dedekind::category::ClassifierApex< S >
	The subobject a predicate classifies, as the pullback of the truth \(\top : 1 \to \Omega\) along the predicate \(p : X \to \Omega\) (the subobject classifier's square): its members, the leg into X their inclusion, the leg to 1 the unique one. A view over the subobject, owning nothing. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsPullback
	The apex of a pullback square over the cospan f: X ⟶ Z, g: Y ⟶ Z: a subobject carrying the two projection legs π₁ ⟶ X, π₂ ⟶ Y.
concept	dedekind::category::IsEqualizer
	The kernel of a parallel pair (f, g: A ⟶ B).
concept	dedekind::category::IsKernelPair
	The pullback of an arrow F against itself — the equivalence relation "have the same F-image" on Dom<F>.
concept	dedekind::category::IsPushout
	The categorical dual of IsPullback: the apex of a pushout square over the span f: Z ⟶ X, g: Z ⟶ Y, carrying the two coprojection colegs ι1: X ⟶ P, ι2: Y ⟶ P.
concept	dedekind::category::IsParallelPair
	F and G are a parallel pair of arrows — shared Dom and shared Cod.

Functions
template<typename L, typename Π, typename F, typename G> requires IsOckhamAlgebra<L> && IsArrow<F> && IsArrow<G> && IsProduct<Π, Dom<F>, Dom<G>> && std::same_as<Cod<F>, Cod<G>> && std::equality_comparable<Cod<F>>
constexpr auto	dedekind::category::make_χ (F f, G g)
	The Characteristic Morphism χ: (X × Y) ⟶ Ω.
template<typename L = Boole, typename Π, typename F_Raw, typename G_Raw>
constexpr auto	dedekind::category::pullback (F_Raw f_raw, G_Raw g_raw)
	The Pullback Factory — constructs the Fiber Product X ×_Z Y.
template<typename S> requires IsSubobject<std::remove_cvref_t<S>, typename std::remove_cvref_t<S>::Domain>
constexpr SubobjectInclusion< std::remove_cvref_t< S > >	dedekind::category::inclusion_arrow (const S &s)
template<typename S> requires IsSubobject<S, typename S::Domain>
constexpr ClassifierApex< S >	dedekind::category::as_classified (const S &s)

Detailed Description

Limits — Equalizers and Fiber Products (Pullbacks).

@partition :pullback

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

@quote "The pullback is the categorical generalisation of the fiber product: it is the universal solution to finding pairs (x, y) that agree in Z." — Saunders Mac Lane, Categories for the Working Mathematician

pullback__Pullbacks_and_Equalizers

This partition defines the two primary limit constructions used in the Dedekind Topos:

• Equalizer (IsEqualizer): The kernel of a parallel pair (f, g: A ⟶ B). Selects exactly those members of A where f and g coincide.
• Pullback (IsPullback, pullback): The Fiber Product X ×_Z Y. Given f: X ⟶ Z and g: Y ⟶ Z, the pullback is a Subobject of X × Y containing exactly those pairs (x, y) where f(x) = g(y).

In this implementation both are realised as Subobject species whose characteristic morphism χ encodes the membership predicate.

pullback__Kernel_Pair_and_Parallel_Pair

Two structurally-named extensions of the above, anchoring the image-as-coequalizer-of-kernel-pair reading the §3 paper outline (Functions on Sets: Filtering and Transforming) refers to:

• Kernel pair (IsKernelPair<P, F>): the pullback of an arrow F against itself, i.e. the equivalence relation "have the same F-image" on Dom<F>. Concretely IsKernelPair<P, F> ≡ IsPullback<P, F, F>; the alias exists to give the kernel-pair role its textbook name at the concept level.
• Parallel pair (IsParallelPair<F, G>): the structural precondition shared by an equalizer's input and a coequalizer's input — two arrows F, G with matching Dom and Cod. Used here as the input shape for the image-as-coequalizer reading: the kernel pair of F supplies two parallel projections π_1, π_2 : P ⇒ Dom<F>, and the image is the coequalizer of that parallel pair.

The full coequalizer concept ( IsCoequalizer<Q, F, G> — IsParallelPair<F, G> && IsQuotient<Q, Cod<F>>) lives in :image alongside IsImageOf, since the image-as-coequalizer reading is the structural payoff that ties the two sides of the canonical epi-mono factorisation together. IsQuotient itself (the dual of IsSubobject, the "co-classifier" surface) lives in :topoi where the subobject classifier already lives.

Wikipedia: Pullback (category theory), Equaliser (mathematics)

Note

"In these days the angel of topology and the devil of abstract algebra fight for the soul of each individual mathematical domain." – Hermann Weyl, Invariants (1939)