vec2.cppm File Reference

Level 12.5a₀: 2-tuples — Vec2 / Vec2V (column) and Covec2V (row). More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.linear_algebra:contracts;
import dedekind.sets;
import dedekind.order;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for vec2.cppm:

Classes
struct	dedekind::linear_algebra::Vec2< T, x, y >
	Structural 2-tuple with coordinates at the type level. More...
struct	dedekind::linear_algebra::Vec2V< T >
	Value-level column vector of length 2, viewed as a 2×1 matrix. More...
struct	dedekind::linear_algebra::Vec2V< T >::ArrowView
	Named-pair view via operator->. More...
struct	dedekind::linear_algebra::Covec2V< T >
	Value-level row vector (covector) of length 2, viewed as a 1×2 matrix. More...
struct	dedekind::linear_algebra::Vec2Map< T, F >
	f on every entry: the vec2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::vec2_functor< T >
struct	dedekind::linear_algebra::Covec2Map< T, F >
	f on every entry: the covec2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::covec2_functor< T >
struct	dedekind::category::is_functorial< dedekind::linear_algebra::vec2_functor< T > >
	Elementwise lifts: the functor laws hold by construction. More...
struct	dedekind::category::is_functorial< dedekind::linear_algebra::covec2_functor< T > >
struct	dedekind::category::unit_witness< dedekind::linear_algebra::vec2_functor< T >, T >
struct	dedekind::category::unit_witness< dedekind::linear_algebra::covec2_functor< T >, T >
struct	dedekind::category::counit_witness< dedekind::linear_algebra::vec2_functor< T >, T >
	Counit / extract witness for Vec2V<T>. Canonical projection to the first coordinate; mirrors the Reader-monad π_0 counit. More...
struct	dedekind::category::product_algebra_base< dedekind::linear_algebra::Vec2V< T > >
struct	dedekind::category::product_algebra_base< dedekind::linear_algebra::Covec2V< T > >
struct	dedekind::category::unit_trait< dedekind::linear_algebra::Vec2V< T >, std::plus< dedekind::linear_algebra::Vec2V< T > > >
struct	dedekind::category::unit_trait< dedekind::linear_algebra::Covec2V< T >, std::plus< dedekind::linear_algebra::Covec2V< T > > >
struct	dedekind::category::inverse_trait< dedekind::linear_algebra::Vec2V< T >, std::plus< dedekind::linear_algebra::Vec2V< T > > >
struct	dedekind::category::inverse_trait< dedekind::linear_algebra::Covec2V< T >, std::plus< dedekind::linear_algebra::Covec2V< T > > >

Namespaces
namespace	dedekind::category

Variables
template<typename T>
constexpr bool	dedekind::category::is_invertible_v< dedekind::linear_algebra::Vec2V< T >, std::plus< dedekind::linear_algebra::Vec2V< T > > > = true
template<typename T>
constexpr bool	dedekind::category::is_invertible_v< dedekind::linear_algebra::Covec2V< T >, std::plus< dedekind::linear_algebra::Covec2V< T > > > = true
template<typename T>
constexpr bool	dedekind::linear_algebra::is_free_module_v< Vec2V< T >, T, 2 > = true
template<typename T>
constexpr bool	dedekind::linear_algebra::is_free_module_v< Covec2V< T >, T, 2 > = true
template<typename T, typename Idx>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Vec2V< T >, Idx >
template<typename T, typename Idx>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Covec2V< T >, Idx > = true
template<typename T, std::integral U, U I>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Vec2V< T >, std::integral_constant< U, I > > = true
template<typename T, std::integral U, U I>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Covec2V< T >, std::integral_constant< U, I > > = true
template<typename T>
constexpr bool	dedekind::category::is_kleisli_deref_v< dedekind::linear_algebra::Vec2V< T > >
constexpr Vec2V< unsigned int >	dedekind::linear_algebra::detail_op::opv {3u, 7u}
constexpr Covec2V< unsigned int >	dedekind::linear_algebra::detail_op::opcv {4u, 9u}

Detailed Description

Level 12.5a₀: 2-tuples — Vec2 / Vec2V (column) and Covec2V (row).

@partition :vec2

Copyright

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

tuple__Motivation

Following Stammbach's "Lineare Algebra", a tuple is a finite, ordered collection of elements in a common carrier: (x₁, …, xₙ) ∈ Tⁿ. Tuples come before matrices in the pedagogical order — matrices will then be interpreted as linear maps between tuple spaces. This partition hosts the tuple-level types:

• Vec2<T, x, y> — NTTP 2-tuple (entries at the type level).
• Vec2V<T> — value-level column 2-tuple (a 2×1 matrix).
• Covec2V<T> — value-level row 2-tuple (a 1×2 matrix).

The column/row orientation tags come from :contracts; transpose exchanges Vec2V ↔ Covec2V, establishing them as a dual pair.

vec2__CT_Framing

In CT lingo: Vec2V<T> = T² is a homogeneous pair — the diagonal image of the binary Cartesian product (Δ: T → T × T from dedekind.category:cartesian) where both factors are the same carrier. This is the textbook P (direct product) of HSP (Burris–Sankappanavar §II.10) at n = 2; the structural- trait propagation in dedekind.algebra:quotient lifts the species traits componentwise from T to Vec2V<T>. The heterogeneous tuple — (A, B) where A and B are distinct carriers — lives in dedekind.category:cartesian (Pierce-land); homogeneous n=2 is what this partition reifies.

Note

"I have in previous papers defined a 'Matrix' as a rectangular array of terms, out of which different systems of determinants may be engendered, as from the womb of a common parent." — James Joseph Sylvester, Additions to the Articles 'On a New Class of Theorems' and 'On Pascal's Theorem', Philosophical Magazine 4th series, vol. 1 (1851), p. 295.

The Sylvester etymology — matrix as mater, "womb" — lands well at the tuple layer: the rank-1 carriers Vec2V<T> (a column) and Covec2V<T> (a row) are the parents from which Matrix2x2V<T> is engendered by horizontal / vertical concatenation.