dedekind::category::Compose< F, G > Struct Template Reference

The reified composition arrow g∘f: "apply @c F, then @c G" (diagrammatic f≫g order), the arrow-algebra companion to Identity. More...

Collaboration diagram for dedekind::category::Compose< F, G >:

Public Types
using	Domain = Dom<F>
using	Codomain = Cod<G>

Public Member Functions
constexpr bool	operator== (const Compose &) const =default
	Equal when the legs are (:cartesian's Arrows).
template<typename X> requires Presents<X, Domain> && requires(const F& f_, const G& g_, const X& x_) { g_(f_(x_)); }
constexpr auto	operator() (const X &x) const
	Run the pipeline (g∘f)(x) = g(f(x)), at any presentation of the domain (morphism__Objects_And_Their_Presentations): two arrows between objects presented by many types compose like any other. Where the result converts to the codomain's value type it is returned as that type, as before.

Public Attributes
F	f
G	g

Detailed Description

template<IsArrow F, IsArrow G>
requires std::same_as<Cod<F>, Dom<G>>
struct dedekind::category::Compose< F, G >

The reified composition arrow g∘f: "apply @c F, then @c G" (diagrammatic f≫g order), the arrow-algebra companion to Identity.

Where Identity is the unit, Compose is the binary that makes composition a first-class type. It is what operator>> returns (f≫g = Compose<F,G>{f,g}); the previous lambda-wrapped arrow<A,C> erased the operand types, whereas Compose keeps F,G in the result type, so it is an IsArrow that downstream reasoning can pattern-match on. Two payoffs it unlocks (#908):

1. Substitution f*: the contravariant pullback preimage(f,P) is P∘f, i.e. Compose<F,P> — the general shape whose closed-form collapses (halfspace, :relational, ...) are the downstream fibres.
2. Variance composition: :posetal registers the Horn clauses co∘co=co and anti∘anti=co (two flips cancel) on Compose, closing the one rule the variance logic program was missing.

Template Parameters

F	the first arrow A→B (applied first).
G	the second arrow B→C (applied second); Cod<F> must be Dom<G>.

---

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

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