cartesian_bicategory.cppm File Reference

The meet is the right adjoint of the diagonal (Δ⊣∧), reified. More...

#include <concepts>
#include <functional>
#include <utility>
#include <variant>
import dedekind.category:cartesian;

Include dependency graph for cartesian_bicategory.cppm:

Classes
struct	dedekind::category::Copy< A >
	Copy (comonoid comultiplication) Δ:A→A×A, a↦(a,a). The left adjoint of the meet; the fan-out of a cartesian bicategory. More...
struct	dedekind::category::Delete< A >
	Delete (counit) ε:A→1. Completes the commutative comonoid. More...
struct	dedekind::category::Merge< A, Meet >
	Merge (the dagger of copy) Δ†:A×A→A, (a,b)↦a⊓b. The right adjoint of the diagonal; the value that IsMeetAsRightAdjoint certifies as the glb. More...
struct	dedekind::category::Tensor< R, S >
	The parallel product ⊗ as the arrow-half of the product bifunctor: R⊗S : A×B→C×D is IsProduct acting on the morphism pair (R,S). The object-half is IsProduct itself (the carrier A×B is the product object); the arrow-half is this Tensor. The action is the mediating morphism ⟨R∘π₁, S∘π₂⟩ built from the product's own reified projections Π<1, P> / Π<2, P> (:limit) and its pairing (the std::pair mediator mediate_product wraps as an arrow); nothing here reimplements the universal property. More...
struct	dedekind::category::MergeBadOp

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsCopy
	: the DIAGONAL notion Δ:A→A×A --- an arrow whose Codomain is the square of its Domain (the comonoid comultiplication / fan-out). Copy is the canonical MODEL; this concept is the matchable "diagonal" handle. Purely structural: it names the crossed A→A×A signature, not that the map is a↦(a,a) (that is Copy's own obligation). Cartesian only: the non-cartesian ⊗ setting needs the carrier generalized past std::pair (#951); a type carrying more than one arrow reading needs the dom/cod contract (#952).
concept	dedekind::category::IsMerge
	: the FOLD notion Δ†:A×A→A --- an arrow whose Domain is the square of its Codomain (the comonoid dagger / binary combiner). Merge<A,Meet> is the canonical MODEL; this concept is the matchable handle. Purely structural: it names the A×A→A signature, so a PROJECTION π:A×A→A also satisfies it (the shape cannot tell a fold from a projection, the same honesty gap as glb-vs-lub). Same seams as IsCopy: carrier past std::pair (#951); the multi-reading dom/cod contract (#952).
concept	dedekind::category::IsMeetAsRightAdjoint
	The STRUCTURAL shape of "the meet @c ∧ is the right adjoint of the diagonal @c Δ" (Δ⊣∧): the reified theory this slice postulates as a type-check.
concept	dedekind::category::IsTensor
	: the structural shape of the parallel product ⊗ --- an arrow whose Domain AND Codomain are product objects (the arrow-half of the product bifunctor). Tensor<R,S> is the canonical MODEL; this concept is the matchable handle. Cartesian only: the non-cartesian monoidal ⊗ (LA outer product) needs the carrier generalized past IsProduct (#951); a type with >1 arrow reading needs the dom/cod contract (#952).

Variables
template<typename A, typename LeqA>
constexpr bool	dedekind::category::is_monotone_v< Copy< A >, ProductLeq< LeqA, LeqA > > = true
template<typename A, typename Meet>
constexpr bool	dedekind::category::is_monotone_v< Merge< A, Meet >, ProductLeq< std::less_equal< A >, std::less_equal< A > > > = true
template<std::totally_ordered P>
constexpr bool	dedekind::category::is_adjoint_v< Copy< P >, Merge< P, Inf >, ProductLeq< std::less_equal< P >, std::less_equal< P > > > = true
	The theorem Δ ⊣ ∧, \(\Delta(a) \le_\times (x, y) \iff a \le x \wedge y\), registered per glb: Inf (min) on a totally ordered carrier under its own ≤, and ∧ on bool. The shape IsMerge cannot tell the glb from the lub (Sup is a monotone fold of the same signature and is not the right adjoint of Δ), so the law leg is where that distinction lives; a merge with another injected op registers its own fact next to the proof that it is the glb.
template<>
constexpr bool	dedekind::category::is_adjoint_v< Copy< bool >, Merge< bool, std::logical_and< bool > >, ProductLeq< std::less_equal< bool >, std::less_equal< bool > > >
template<typename R, typename S, typename LeqR, typename LeqS>
constexpr bool	dedekind::category::is_monotone_v< Tensor< R, S >, ProductLeq< LeqR, LeqS > >
template<typename R, typename S, typename LeqR, typename LeqS>
constexpr bool	dedekind::category::is_antimonotone_v< Tensor< R, S >, ProductLeq< LeqR, LeqS > >

Detailed Description

The meet is the right adjoint of the diagonal (Δ⊣∧), reified.

@partition :cartesian_bicategory

Copyright

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

Meet as the adjoint of the diagonal

Sketch (epic #946, slice S0). Reifies the theory Δ ⊣ ∧ as a concept first (IsMeetAsRightAdjoint), so the composite meet = Δ† ∘ (⊗) ∘ Δ must type-check against it. In a cartesian bicategory (Carboni & Walters) every object carries a commutative comonoid: copy Δ:A→A×A, delete ε:A→1, and the dagger merge Δ†:A×A→A; the meet is that merge, and "meet @c = @c right @c adjoint @c of @c Δ" is its 1-categorical shadow (Mac Lane, adjunctions in a poset degenerate to Galois connections).

What is compiled here

A compiled, type-checked partition. :lattice_term imports it and static_asserts IsMeetAsRightAdjoint over its canonical carrier, so the reification is load-bearing early rather than an orphan. This file provides the bicategory STRUCTURE — the comonoid legs Copy / Merge / Delete and the arrow-level product (⊗) (Tensor) — plus the Δ⊣∧ concept. The composite meet Δ† ∘ (⊗) ∘ Δ that is built FROM this structure is the relational intersection Intersect, and lives in :relational:dyadic (next to the extensional R∩S it realises point-free).

Wikipedia: Cartesian bicategory, Frobenius algebra, Adjoint functors

Note

"Only connectivity matters." Bob Coecke & Aleks Kissinger, Picturing Quantum Processes (Cambridge, 2017), on spider fusion: the copy / merge Frobenius maps compose by their wiring alone, which is exactly why the meet falls out of the comonoid structure rather than the carrier.

See also

#275 nLab algebra/category hierarchy (work in progress): the monoidal category with its coherence data beyond the cartesian IsTensor (see also #951).