category.cppm

Go to the documentation of this file.

 
export module dedekind.category;
 
// Level 0: The Taxonomic Bricks (Atoms)
export import :species;      // The Raw Machine Data
export import :morphism;     // The Base Arrow (Prerequisite for everything)
export import :involution;   // f∘f = id — the dagger seed (converse/transpose;
                             // future home of the †-category / unitary surface)
export import :mereology;    // Parthood (Prerequisite for Logic/Sets)
export import :equivalence;  // Equivalence relations (Mazur up-to relaxation;
                             // #591)
export import :logic;        // The Subobject Classifier (Truth)
 
// Level 0.5: The Structural Infrastructure
export import :thin;          // Thin Categories (preorders; row 1 of the
                              // lattice Form-chain; #698)
export import :posetal;       // Partial Orders (thin + antisymmetric)
export import :filtered;      // Filtered Categories (thin + directed; row 3
                              // of the lattice Form-chain; #698 Slice 2)
export import :lattice;       // Lattice Categories (posetal + filtered +
                              // cofiltered + universality; row 4 of the
                              // lattice Form-chain; #698 Slice 3)
export import :lattice_term;  // Generic lattice-law term reducer (compile-time
                              // normal form over <L,∧,∨,⊤,⊥,¬>; #865/#888/#890)
export import :small;         // Small Categories
export import :discrete;      // The Discrete Category (Points as Arrows)
export import :nno;        // The Natural Numbers Object (ETCS Axiom 9 reified;
                           // closes part of #445)
export import :chain;      // Dedekind's chain as a range (#981)
export import :limit;      // Universal Limits
export import :cartesian;  // Products/Coproducts, CCC Foundations
export import :topoi;      // Internal Logic of the Topos
export import :pullback;   // The Universal Construction "Sink"
export import :factorisation;  // (Regular epi, mono) factorisation system,
                               // IsRegularCategory / IsExactCategory; row 4–8
                               // of the quotient Form-chain (#718).
export import :image;          // IsImageOf<S, F> — image of an arrow as
                               // a structurally-named subobject of Cod<F>;
                               // mono side of the canonical epi-mono
                               // factorisation.  The dual quotient side
                               // awaits an IsQuotient sister to IsSubobject;
                               // see :pullback's partition header.
 
// Level 1: The Ideal (Total Algebra)
export import :total;
export import :action;
 
// Level 2: The Bridge (Functorial Spine)
export import :functor;
export import :f_algebra;  // Initial F-algebra / terminal F-coalgebra
                           // universal-property reification (Pierce §5; closes
                           // #449)
export import :natural;
export import :iso;         // Retract / iso-enabling surface (Kleisli into the
                            // maybe monad): IsRetractableArrow, IsoRetract,
                            // blanket iso retract.  Downstream of :natural for
                            // Maybe / η.
export import :adjunction;  // Free / Forgetful pair, IsAdjunction (Pierce-style
                            // separate section)
export import :cartesian_bicategory;  // Frobenius spider: Copy/Merge/Tensor,
                                      // meet = right adjoint of the diagonal
                                      // (Δ ⊣ ∧); reusable downstream (#946)
export import :periodic;       // Periodic arrows on the counts and their counts
export import :runs;           // Run lists over a finite chain: the canonical
                               // form of a decidable set on it (#1135)
export import :comprehension;  // Monad comprehensions: where, select, the
                               // queries of SQL (the Jlt paper's tensor
                               // exhibit, #1104)
export import :automaton;      // The matcher specialised to a set of words:
                               // the minimal automaton, canonical (#1135)
export import :monad;
export import :kleisli;
 
// Level 3: The Reality (Hardware -> Abstraction)
export import :numeric;  // Concrete Hardware Logic (IEEE 754)
export import :partial;  // The Final Abstracted Partial Interface
 
// Level 4: The Skeletal Signatures (Synthesis)
export import :concrete;  // Concreteness layer (IsSubobject, IsConcrete,
                          // χ-based set ops) — re-homed from :etcs (#636);
                          // prerequisite for the ETCS axioms below.
export import :etcs;      // The World of Sets (Importing Partial + Mereology)
 
namespace dedekind::category {
// Top-level category-theoretic aliases and universal compositions.
}