/// Limits and Colimits in Category Theory.
///
/// A limit is a universal construction that "combines" a diagram of objects
/// into a single object with projections.
/// A colimit is the dual — it "combines" a diagram with injections.
///
/// In the category of types (Hask/Rust):
///
/// Limits:
/// Product = (A, B) — binary limit of {A, B}
/// Equaliser = { x | f(x) = g(x) }
/// Pullback = { (a,b) | f(a) = g(b) }
/// Terminal = ()
///
/// Colimits:
/// Coproduct = Either<A,B> — binary colimit of {A, B}
/// Coequaliser = quotient
/// Pushout = colimit of a span
/// Initial = ! (Never / Void)
///
/// These are foundational — every data type is a limit or colimit.
// ── Products (Binary Limits) ─────────────────────────────────────────────────
/// Product introduction: given A and B, produce (A, B).
fn product<A, B>(a: A, b: B) -> (A, B) {
(a, b)
}
/// Product projections (the "legs" of the limit cone).
fn proj1<A: Clone, B>(p: &(A, B)) -> A { p.0.clone() }
fn proj2<A, B: Clone>(p: &(A, B)) -> B { p.1.clone() }
/// Universal property of the product:
/// Any function `h: X -> (A, B)` factors uniquely as `product(f, g)` where
/// `f = proj1 . h` and `g = proj2 . h`.
fn pair_of<X: Clone, A, B>(
f: impl Fn(X) -> A,
g: impl Fn(X) -> B,
) -> impl Fn(X) -> (A, B) {
move |x| (f(x.clone()), g(x))
}
// ── Coproducts (Binary Colimits) ─────────────────────────────────────────────
/// Coproduct type.
#[derive(Debug, Clone, PartialEq)]
pub enum Coprod<A, B> {
Inl(A),
Inr(B),
}
/// Coproduct injections (the "legs" of the colimit cocone).
fn inl<A, B>(a: A) -> Coprod<A, B> { Coprod::Inl(a) }
fn inr<A, B>(b: B) -> Coprod<A, B> { Coprod::Inr(b) }
/// Universal property of the coproduct:
/// Any two functions `f: A -> X` and `g: B -> X` give a unique
/// `Either<A,B> -> X` (the "copairing").
fn copair<A, B, X>(
f: impl Fn(A) -> X,
g: impl Fn(B) -> X,
) -> impl Fn(Coprod<A, B>) -> X {
move |c| match c {
Coprod::Inl(a) => f(a),
Coprod::Inr(b) => g(b),
}
}
// ── Terminal object ───────────────────────────────────────────────────────────
/// Terminal object = () : there is exactly one morphism A -> () for any A.
fn terminal<A>(_a: A) -> () {}
// ── Initial object ────────────────────────────────────────────────────────────
/// Initial object = Void (Never): there is exactly one morphism Void -> A,
/// but Void has no inhabitants.
/// In Rust: std::convert::Infallible
fn from_initial(v: std::convert::Infallible) -> i32 {
// This function has no body reachable — it's never called.
match v {}
}
// ── Equaliser (limit of a parallel pair) ─────────────────────────────────────
/// Equaliser of f and g: all x where f(x) = g(x).
fn equaliser<A: Clone, B: PartialEq>(
xs: &[A],
f: impl Fn(&A) -> B,
g: impl Fn(&A) -> B,
) -> Vec<A> {
xs.iter().filter(|x| f(x) == g(x)).cloned().collect()
}
// ── Pullback (limit of a cospan) ─────────────────────────────────────────────
/// Pullback of f: A -> C and g: B -> C:
/// { (a, b) | f(a) = g(b) }
fn pullback<A: Clone, B: Clone, C: PartialEq>(
as_: &[A],
bs: &[B],
f: impl Fn(&A) -> C,
g: impl Fn(&B) -> C,
) -> Vec<(A, B)> {
let mut result = Vec::new();
for a in as_ {
for b in bs {
if f(a) == g(b) {
result.push((a.clone(), b.clone()));
}
}
}
result
}
// ── Coequaliser (colimit of a parallel pair) ─────────────────────────────────
/// Coequaliser of f and g: quotient that identifies f(x) with g(x).
/// We model this as a partition: elements with the same "equivalence class" are merged.
/// Representative: smallest element in each class (under mod-based grouping).
fn coequaliser_classes<A: Clone + Ord>(
xs: &[A],
f: impl Fn(&A) -> usize,
g: impl Fn(&A) -> usize,
) -> Vec<(usize, Vec<A>)> {
use std::collections::HashMap;
let mut classes: HashMap<usize, Vec<A>> = HashMap::new();
for x in xs {
// Both f(x) and g(x) are in the same equivalence class
let key = f(x).min(g(x));
classes.entry(key).or_default().push(x.clone());
}
let mut result: Vec<(usize, Vec<A>)> = classes.into_iter().collect();
result.sort_by_key(|(k, _)| *k);
result
}
fn main() {
println!("=== Limits and Colimits ===\n");
println!("Limits: product, equaliser, pullback, terminal");
println!("Colimits: coproduct, coequaliser, pushout, initial\n");
// ── Products ──────────────────────────────────────────────────────────────
println!("── Products (Limits) ──\n");
let p = product(3_i32, "hello");
println!("product(3, \"hello\") = ({}, \"{}\")", proj1(&p), proj2(&p));
let both = pair_of(|x: i32| x * 2, |x: i32| x + 10);
let (a, b) = both(5);
println!("pair_of(*2, +10) applied to 5 = ({}, {})", a, b);
// ── Coproducts ────────────────────────────────────────────────────────────
println!("\n── Coproducts (Colimits) ──\n");
let x: Coprod<i32, &str> = inl(42);
let y: Coprod<i32, &str> = inr("hello");
let describe = copair(
|n: i32| format!("number {}", n),
|s: &str| format!("string \"{}\"", s),
);
println!("inl(42): {}", describe(x));
println!("inr(\"hello\"): {}", describe(y));
// ── Terminal ──────────────────────────────────────────────────────────────
println!("\n── Terminal Object ──\n");
println!("terminal(42) = {:?}", terminal(42));
println!("terminal(\"anything\") = {:?}", terminal("anything"));
println!("There is exactly one morphism A -> () for any A.");
// ── Equaliser ─────────────────────────────────────────────────────────────
println!("\n── Equaliser ──\n");
let nums = vec![0_i32, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12];
let eq = equaliser(&nums, |x| x % 2, |x| x % 3);
println!("equaliser (x mod 2 = x mod 3) on 0..12: {:?}", eq);
// x mod 2 = x mod 3 for x in {0, 6, 12} (when both are 0)
// ── Pullback ──────────────────────────────────────────────────────────────
println!("\n── Pullback ──\n");
let evens = vec![2_i32, 4, 6, 8];
let words = vec!["ab", "cd", "abcd", "x"];
let pb = pullback(&evens, &words, |n| *n as usize, |s| s.len());
println!("pullback (length) of evens and words: {:?}", pb);
// ── Coequaliser ───────────────────────────────────────────────────────────
println!("\n── Coequaliser ──\n");
let vals = vec![1_i32, 2, 3, 4, 5, 6];
let classes = coequaliser_classes(&vals, |x| *x as usize % 3, |x| (*x + 1) as usize % 3);
println!("coequaliser (mod 3, mod 3 +1) classes:");
for (k, v) in &classes {
println!(" class {}: {:?}", k, v);
}
println!();
println!("Universal properties:");
println!(" Product: any cone (f: X->A, g: X->B) factors through (A×B)");
println!(" Coproduct: any cocone (f: A->X, g: B->X) factors through (A+B)");
println!(" These are the 'most efficient' ways to combine/split types.");
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_product_projections() {
let p = product(10_i32, "hello");
assert_eq!(proj1(&p), 10);
assert_eq!(proj2(&p), "hello");
}
#[test]
fn test_pair_of() {
let f = pair_of(|x: i32| x * 2, |x: i32| x + 1);
assert_eq!(f(5), (10, 6));
}
#[test]
fn test_coproduct_inl() {
let x: Coprod<i32, &str> = inl(42);
let r = copair(|n: i32| n * 2, |_: &str| 0)(x);
assert_eq!(r, 84);
}
#[test]
fn test_coproduct_inr() {
let x: Coprod<i32, &str> = inr("hello");
let r = copair(|_: i32| 0, |s: &str| s.len())(x);
assert_eq!(r, 5);
}
#[test]
fn test_equaliser() {
let nums = vec![0_i32, 1, 2, 3, 4, 5, 6];
let eq = equaliser(&nums, |x| x % 2, |x| x % 3);
// mod 2 = mod 3 at 0 (0=0), 6 (0=0)
assert!(eq.contains(&0));
assert!(eq.contains(&6));
}
#[test]
fn test_pullback() {
let as_ = vec![2_i32, 4, 6];
let bs = vec!["ab", "abcd", "x"];
let pb = pullback(&as_, &bs, |n| *n as usize, |s| s.len());
assert!(pb.contains(&(2, "ab")));
assert!(pb.contains(&(4, "abcd")));
}
}
(* Limits and colimits are universal constructions in category theory.
Products = binary limits; Coproducts = binary colimits.
In types: products = tuples, coproducts = sum types *)
(* Product = limit of discrete diagram {A, B} *)
(* Characterised by projections fst, snd *)
let product_intro a b = (a, b)
let fst (a, _) = a
let snd (_, b) = b
(* Universality: any cone factors uniquely through the product *)
let pair_of f g x = (f x, g x)
(* Coproduct = colimit of discrete diagram {A, B} *)
type ('a, 'b) coprod = Inl of 'a | Inr of 'b
let coprod_inl a = Inl a
let coprod_inr b = Inr b
(* Universality: any cocone factors through the coproduct *)
let coprod_elim f g = function Inl a -> f a | Inr b -> g b
(* Equaliser = limit of parallel arrows *)
(* { x | f(x) = g(x) } *)
let equaliser f g lst = List.filter (fun x -> f x = g x) lst
(* Coequaliser = colimit *)
(* Quotient: identify elements where f(x) = f(y) -> same class *)
let coequaliser f lst =
let module M = Map.Make(Int) in
List.fold_left (fun m x -> M.add (f x) x m) M.empty lst
|> M.bindings |> List.map snd
let () =
Printf.printf "product (3,4): fst=%d snd=%d\n" (fst (3,4)) (snd (3,4));
let both = pair_of (fun x -> x * 2) (fun x -> x + 10) in
Printf.printf "pair_of: %s\n" (let (a,b) = both 5 in Printf.sprintf "(%d,%d)" a b);
let sum_or_str = coprod_elim string_of_int (fun s -> s ^ "!") in
Printf.printf "coprod Inl 42: %s\n" (sum_or_str (Inl 42));
Printf.printf "coprod Inr hi: %s\n" (sum_or_str (Inr "hi"));
let eq = equaliser (fun x -> x mod 2) (fun x -> x mod 3) [0;1;2;3;4;5;6;12] in
Printf.printf "equaliser mod2=mod3: [%s]\n" (eq |> List.map string_of_int |> String.concat ";")