dedekind::category::IsEqualizer Concept Reference

The kernel of a parallel pair (f, g: A ⟶ B). More...

Concept definition

template<typename E, typename F, typename G>
concept dedekind::category::IsEqualizer = 
    IsArrow<F> && IsArrow<G> && std::same_as<Dom<F>, Dom<G>> &&
    std::same_as<Cod<F>, Cod<G>> && IsSubobject<E, Dom<F>>

Detailed Description

The kernel of a parallel pair (f, g: A ⟶ B).

In the Dedekind Topos, an Equalizer is a Subobject E ↣ A containing exactly those members where the morphisms f and g coincide. It is the internal "Solution Set" for the equation f(x) = g(x).

pullback__Universal_Property

For any object Q and morphism q: Q ⟶ A such that f ∘ q = g ∘ q, there exists a unique morphism u: Q ⟶ E such that ι ∘ u = q.

Template Parameters

E	The candidate Equalizer species. Must satisfy IsSubobject<E, typename F::Domain>, guaranteeing: an inclusion ι: E ↣ A into the shared domain A, a characteristic morphism χ: A ⟶ Ω (an IsPredicate) with Dom<χ> == A, classifying the solution set.
F	The first parallel morphism f: A ⟶ B.
G	The second parallel morphism g: A ⟶ B.