image.cppm File Reference

Image-as-coequalizer-of-kernel-pair: IsImageOf<S, F> on the mono side and IsCoequalizer<Q, F, G> on the quotient side. More...

#include <concepts>
#include <optional>
#include <type_traits>
#include <utility>
import dedekind.category:logic;

Include dependency graph for image.cppm:

Classes
struct	dedekind::category::ImageChi< F >
	The characteristic predicate of image_of(F) — recognises y as "in the image of @c F". More...
struct	dedekind::category::ImageChi< F >
	Image classifier for a retractable arrow: y is in the image iff the retract fires at y. More...
struct	dedekind::category::image_decidability_witness::ToyRetract
struct	dedekind::category::image_decidability_witness::ToyEmbed
struct	dedekind::category::image_decidability_witness::ToyGeneral
struct	dedekind::category::kernel_quotient< F >
	Opt-in trait: textbook claim "for this @c F, @c A/ker(F) is the carrier @c ::Class". More...
struct	dedekind::category::image_carrier< F >
	Opt-in trait: textbook claim "for this @c F, @c im(F) is the carrier @c ::type". More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsImageOf
	S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi, mono) factorisation system pinned in :factorisation.
concept	dedekind::category::IsCoequalizer
	The categorical dual of IsEqualizer — a Quotient of Cod<F> equating two parallel arrows F, G.
concept	dedekind::category::WitnessesFirstIso
	Connector witnesses the First Isomorphism Theorem at homomorphism F.

Functions
template<typename F> requires IsArrow<F> && std::constructible_from<std::remove_cvref_t<F>, F&&>
constexpr auto	dedekind::category::image_of (F f)
	Factory: image_of(f) constructs the image of f as a Subobject of Cod<F>.
constexpr ToyRetract	dedekind::category::image_decidability_witness::retract (ToyEmbed)

Variables
template<typename A>
constexpr bool	dedekind::category::is_exact_category_v< CanonicalSetCCC< A > > = true
template<>
constexpr bool	dedekind::category::is_monic_arrow_v< image_decidability_witness::ToyEmbed >

Detailed Description

Image-as-coequalizer-of-kernel-pair: IsImageOf<S, F> on the mono side and IsCoequalizer<Q, F, G> on the quotient side.

@partition :image

Copyright

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

image__Motivation

Hosts the canonical epi-mono factorisation chain set up by :pullback (kernel pair, parallel pair) and :topoi (subobject, quotient):

IsKernelPair → IsParallelPair → IsCoequalizer → IsImageOf

For an arrow F : A → B, the image Im(F) is the coequalizer of the kernel pair of F:

\(\mathrm{Im}(F) \) \(=\) \(\mathrm{coeq}(\pi_1, \pi_2 : \mathrm{KernelPair}(F) \rightrightarrows A)\).

Equivalently (in a topos) the image is the smallest subobject of B through which F factors, giving the canonical epi-mono factorisation F = m ∘ e:

A → Im(F) → B

with e regular-epi (the coequalizer projection) and m mono (the inclusion of the image into the codomain). Two structurally named concepts pin the two sides:

• mono side: IsImageOf<S, F> — S is a Subobject of Cod<F> realising the image.
• quotient side: IsCoequalizer<Q, F, G> — Q is a Quotient of Cod<F> equating the parallel pair F, G.

Both are co-located here in :image since the image-as-coequalizer reading is the structural payoff that ties them together. The universal-property obligations (smallest such subobject, canonical factorisation, regular-epi universality of q) remain the engineer's honesty obligation in the IsNNO style.

image__Structural_vs_Universal

What IsImageOf can pin (structural shape):

• F is an arrow ( IsArrow<F>),
• S is a Subobject of Cod<F> ( IsSubobject<S, Cod<F>>).

What IsImageOf cannot pin (engineer's honesty obligation, as for IsNNO):

• That S is the smallest such subobject (universality of the image factorisation),
• That F factors through S as m ∘ e with e regular-epi and m mono,
• That the factorisation is unique up to isomorphism.

C++ concepts cannot quantify over the universal property's $\forall$; they can only pin operational signatures. The naming here is the structural anchor — a downstream carrier witness declares IsImageOf<MyImageSet, MyArrow> to record the intent that its subobject realises the image. The audit (that this is in fact the smallest containing subobject) lives in the witness's documentation and review.

image__Realisation_Regimes

The §3 paper outline (Functions on Sets: Filtering and Transforming) names three realisation regimes for the abstract image, each pinned by IsImageOf with a different S:

• Extensional (finite carriers): S is a concrete std-container subobject realised by iteration in sets:extensional ( image(f, std::unordered_set<T>) etc.).
• Intensional (NNO-domain transforms): S is the orbit closure of an iterated step, naturally pinnable on Path<T> in sequences:path (categorical-anchor breadcrumbs land in the follow-up slice).
• Symbolic (Tier C, future): S is a deferred set expression under an inhabitancy DSL (#603), evaluated lazily.

image__Layering

Upstream-of-everything-numeric. Lives in :category alongside :pullback; carrier witnesses register downstream where the carriers are available ( sets:extensional for std-container carriers; sequences:path for the NNO-morphism reading).

Note

"ἁρμονία δὲ πολυμιγέων ἕνωσις καὶ δίχα φρονεόντων συμφρόνησις." ("Harmony is the unification of things many-mixed, and the same-mindedness of things thinking-apart.") — Philolaus of Croton, fragment B10 DK, apud Stobaeus, Anthology I.21.7d.