dedekind::relational::detail_hyperdoctrine_witness::Copy< A > Struct Template Reference

Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory. More...

Public Types
using	Domain = A
using	Codomain = std::pair<A, A>

Public Member Functions
constexpr Codomain	operator() (const A &a) const
	Fan the input out onto both legs Δ(a)=(a,a).

Detailed Description

template<typename A>
struct dedekind::relational::detail_hyperdoctrine_witness::Copy< A >

Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory.

Meet as the adjoint of the diagonal

Thesis. Lattice reduction ({x>5}∩{x>3} → {x>5}) is order-theoretic, not set-theoretic. The meet is the greatest lower bound, fixed by the order alone; the powerset Sub(A) is merely one model that realises it. So the reduction needs only a poset (a thin category) plus a category-level handle on the glb, and set theory stays downstream as an injected model. The apparent circular dependency ("the category layer would need @c Sub(A) to reduce") is a category error between the two lattices.

The comonoid. In a cartesian bicategory every object carries a commutative comonoid: copy Δ:A→A⊗A (a↦(a,a)) and delete ε:A→1, plus the dagger merge Δ†:A⊗A→A. Then

R ∩ S = Δ† ∘ (R⊗S) ∘ Δ (copy the input, run both, merge where they agree).

Two shadows of one structure.

• Order-adjoint: the copy Δ is the diagonal Δ:P→P×P; its right adjoint (the merge) is the meet. "meet @c = @c right @c adjoint @c of @c Δ" is the 1-categorical shadow. In a poset an adjunction degenerates to a Galois connection (see IsGaloisConnection), so Δ(c)≤(a,b) ⟺ c≤a∧b, which (since Δc=(c,c) under the product order) unfolds to the glb universal property c≤a and c≤b ⟺ c≤a∧b.
• Set: Rel restricted to Sub(A) is one cartesian bicategory; its meet is this general Δ†∘(⊗)∘Δ instantiated.

Why no cycle. The copy Δ here is a function A→A×A, NOT the relational identity Δ={(a,a)} in :relational (which is a↦a, the ; unit, and which imports dedekind.category and so cannot be hoisted). Defining copy/merge in :category, upstream of :sets and :relational, keeps the DAG acyclic: the reducer injects the order algebra (the existing reduce<Term,Ord,Combine> already does this), so no downstream set machinery is pulled upstream.

Honest asymmetry. The meet ∩ falls out of the comonoid. The join ∨ needs more than bare Frobenius (a bicategory of relations); it is NOT in this sketch. FIXME(#946): pin the ∨ story.

Template Parameters

A	the carrier object.

Member Function Documentation

operator()()

template<typename A>

Codomain dedekind::category::Copy< A >::operator() ( const A & a ) const

inlineconstexpr

Fan the input out onto both legs Δ(a)=(a,a).

Parameters

a	the value to copy.

Returns

the diagonal pair (a,a).

Note

The requires clause gates A on std::copy_constructible: the diagonal duplicates its input, so a move-only A removes operator() from the overload set and IsArrow (hence IsCopy) rejects Copy at the concept surface rather than only when the {a,a} body is later instantiated (#950 review). Same guard as Merge::operator() on its injected op.

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/category/cartesian_bicategory.cppm