use crate as pr4xis;
use crate::ontology::{Axiom, Ontology};
pr4xis::ontology! {
name: "CategoryTheory",
source: "Mac Lane (1971); Awodey (2010); Bénabou (1967); Leinster (2004); Eilenberg & Moore (1965); Kleisli (1965); Moggi (1991); Wadler (1992); McBride & Paterson (2008); Meijer-Fokkinga-Paterson (1991); Liang-Hudak-Jones (1995); Yoneda (1954); Ore (1944)",
concepts: [
Object,
Morphism,
Composition,
Identity,
Source,
Target,
Kind,
Endomorphism,
Isomorphism,
Automorphism,
Monomorphism,
Epimorphism,
CategoryStructure,
Functor,
Endofunctor,
NaturalTransformation,
Adjunction,
Unit,
Counit,
Bicategory,
TwoCategory,
HigherCategory,
Applicative,
Monad,
Comonad,
Pure,
Multiplication,
Comultiplication,
Semigroup,
Monoid,
MonoidalCategory,
Tensor,
Product,
Coproduct,
Terminal,
InitialObject,
OppositeCategory,
KleisliCategory,
Algebra,
Coalgebra,
StructureMap,
StateMonad,
ReaderMonad,
WriterMonad,
FreeMonad,
MonadTransformer,
YonedaEmbedding,
Representable,
GaloisConnection,
Interpretation,
InstanceFunctor,
SchemaCategory,
Syntactic,
Semantic,
],
labels: {
Object: ("en", "Object", "A 0-cell inside a category — the basic entity. Mac Lane (1971) CWM Ch. I §1."),
Morphism: ("en", "Morphism / Arrow", "A 1-cell — directed structure-preserving map between objects. Mac Lane uses 'morphism' primary, 'arrow' synonym; Awodey (2010) uses 'arrow' primary."),
Composition: ("en", "Composition", "Given f: A → B and g: B → C, produces g ∘ f: A → C. Mac Lane (1971) Ch. I §1."),
Identity: ("en", "Identity morphism", "For every object A, id_A: A → A that is left and right neutral for composition. Mac Lane (1971) Ch. I §1."),
Source: ("en", "Source", "The domain of a morphism — what it comes from."),
Target: ("en", "Target", "The codomain of a morphism — what it goes to."),
Kind: ("en", "Relation kind", "The named relation-type tag carried by every morphism per OBO-RO (Smith et al. 2005)."),
Endomorphism: ("en", "Endomorphism", "A morphism whose source and target are the same object. Mac Lane (1971) Ch. I §5."),
Isomorphism: ("en", "Isomorphism", "A morphism with a two-sided inverse. Mac Lane (1971) Ch. I §5."),
Automorphism: ("en", "Automorphism", "An isomorphism that is also an endomorphism. Mac Lane (1971) Ch. I §5."),
Monomorphism: ("en", "Monomorphism", "A left-cancellative morphism. Mac Lane (1971) Ch. I §5."),
Epimorphism: ("en", "Epimorphism", "A right-cancellative morphism. Mac Lane (1971) Ch. I §5."),
CategoryStructure: ("en", "Category", "Objects + morphisms + composition + identity satisfying the category laws. Mac Lane (1971) Ch. I §1."),
Functor: ("en", "Functor", "A 1-cell in Cat — structure-preserving map between categories. Mac Lane (1971) Ch. II §1."),
Endofunctor: ("en", "Endofunctor", "A functor F: C → C whose source and target categories coincide. Mac Lane (1971) Ch. II §1; foundation for monads/algebras."),
NaturalTransformation: ("en", "Natural transformation", "A 2-cell in Cat — a map between parallel functors. Mac Lane (1971) Ch. II §4."),
Adjunction: ("en", "Adjunction", "A structured pair F ⊣ G with unit and counit satisfying triangle identities. Mac Lane (1971) Ch. IV §1."),
Unit: ("en", "Unit", "A natural transformation η: 1 ⇒ T (for a monad T) or η: 1 ⇒ G∘F (for an adjunction F ⊣ G). Mac Lane (1971) Ch. IV §1."),
Counit: ("en", "Counit", "A natural transformation ε: T ⇒ 1 (for a comonad T) or ε: F∘G ⇒ 1 (for an adjunction). Mac Lane (1971) Ch. IV §1."),
Bicategory: ("en", "Bicategory", "A weak 2-category — associativity/identity up to coherent 2-isomorphism. Bénabou (1967)."),
TwoCategory: ("en", "2-category", "Cat is a 2-category: 0-cells are categories, 1-cells functors, 2-cells nat-trans. Mac Lane (1971) XII.3."),
HigherCategory: ("en", "Higher category", "An n-category generalising 2-categories. Leinster (2004)."),
Applicative: ("en", "Applicative functor", "An endofunctor with `pure` and `ap` — supports context-free effectful composition. McBride & Paterson (2008)."),
Monad: ("en", "Monad", "A monoid in the category of endofunctors — (T, η, μ) satisfying unit and associativity laws. Moggi (1991); Wadler (1992); Mac Lane (1971) Ch. VI."),
Comonad: ("en", "Comonad", "Dual of a monad — (T, ε, δ) with counit and comultiplication. Mac Lane (1971) Ch. VI §4."),
Pure: ("en", "Pure / Return / Unit-morphism", "The lifting A → F(A) provided by an Applicative or Monad."),
Multiplication: ("en", "Multiplication (μ)", "The monad's natural transformation μ: T∘T ⇒ T (collapse two layers into one). Moggi (1991)."),
Comultiplication: ("en", "Comultiplication (δ)", "The comonad's natural transformation δ: T ⇒ T∘T (split into two layers)."),
Semigroup: ("en", "Semigroup", "A set with an associative binary operation. Foundational algebraic structure, predating Monoid."),
Monoid: ("en", "Monoid", "A semigroup with an identity element. Mac Lane (1971) Ch. III §6; monads are monoids in the endofunctor category."),
MonoidalCategory: ("en", "Monoidal category", "A category equipped with a tensor product ⊗ and unit I, satisfying coherence laws. Mac Lane (1971) Ch. VII."),
Tensor: ("en", "Tensor product (⊗)", "The bifunctor ⊗: C × C → C of a monoidal category. Mac Lane (1971) Ch. VII."),
Product: ("en", "Product (×)", "A limit of a two-object diagram — paired with projections. Mac Lane (1971) Ch. III §4."),
Coproduct: ("en", "Coproduct (+)", "Dual of product — a colimit with injections. Mac Lane (1971) Ch. III §4."),
Terminal: ("en", "Terminal object", "An object 1 such that there is exactly one morphism A → 1 from every object. Mac Lane (1971) Ch. III §3."),
InitialObject: ("en", "Initial object", "Dual of terminal — an object 0 with exactly one morphism 0 → A to every object. Mac Lane (1971) Ch. III §3."),
OppositeCategory: ("en", "Opposite category (C^op)", "The dual category: same objects, morphisms reversed. Mac Lane (1971) Ch. II §2."),
KleisliCategory: ("en", "Kleisli category", "For a monad T on C, the category whose morphisms A → B are C-morphisms A → T(B). Kleisli (1965)."),
Algebra: ("en", "F-algebra", "Pair (A, α: F(A) → A) where F is an endofunctor. Meijer-Fokkinga-Paterson (1991); initial algebras characterise recursive types."),
Coalgebra: ("en", "F-coalgebra", "Pair (A, α: A → F(A)) — dual of F-algebra. Characterises corecursive / infinite structures."),
StructureMap: ("en", "Structure map", "The defining morphism of an F-(co)algebra: α: F(A) → A (algebra) or α: A → F(A) (coalgebra)."),
StateMonad: ("en", "State monad", "S → (A, S) — threads mutable state through pure computations. Wadler (1992); Liang-Hudak-Jones (1995)."),
ReaderMonad: ("en", "Reader monad", "R → A — reads from a fixed environment. Wadler (1992)."),
WriterMonad: ("en", "Writer monad", "(A, W) with W a monoid — accumulates output alongside computation. Wadler (1992); pr4xis's `Traced` specialises it."),
FreeMonad: ("en", "Free monad", "The initial algebra of the functor T(A) = A + F(T(A)) — universal among monads over F."),
MonadTransformer: ("en", "Monad transformer", "A type constructor T such that if M is a monad then T(M) is also a monad — composes monadic effects. Liang-Hudak-Jones (1995)."),
YonedaEmbedding: ("en", "Yoneda embedding", "The functor y: C → [C^op, Set] sending A to Hom(-, A). Fully faithful — an object IS its representable. Yoneda (1954)."),
Representable: ("en", "Representable functor", "A functor naturally isomorphic to Hom(A, -) for some A. Yoneda (1954); Mac Lane (1971) Ch. III §2."),
GaloisConnection: ("en", "Galois connection", "An adjunction between posets — a pair (f ⊣ g) of monotone maps on partially-ordered sets. Ore (1944); special case of Mac Lane's adjunction."),
Interpretation: ("en", "Interpretation functor", "A functor that gives semantic meaning to a syntactic structure — maps from a syntactic/theory category to a semantic category. Lambek & Scott (1986); Goguen & Burstall (1984) institutions."),
InstanceFunctor: ("en", "Instance functor", "Spivak (2012) FDM §3: a functor I: S → Set from a schema category S to Set — each object's image is the set of instances, each morphism's image is the function between those sets. Characterises database-instance semantics of schema categories."),
SchemaCategory: ("en", "Schema category", "Spivak (2012) FDM: a finitely-presented category encoding a database schema — objects are tables, morphisms are foreign-key paths, path equivalences are schema constraints."),
Syntactic: ("en", "Syntactic side", "The formal-structure source of an interpretation — schema, theory, type system. Lambek & Scott (1986) — the category where propositions/types live formally."),
Semantic: ("en", "Semantic side", "The model / meaning-carrying target of an interpretation — Set for instances, a model category for logical semantics. Tarski (1936); Lambek-Scott (1986)."),
},
is_a: [
(Endomorphism, Morphism),
(Isomorphism, Morphism),
(Automorphism, Endomorphism),
(Automorphism, Isomorphism),
(Monomorphism, Morphism),
(Epimorphism, Morphism),
(Functor, Morphism),
(Endofunctor, Functor),
(NaturalTransformation, Morphism),
(Unit, NaturalTransformation),
(Counit, NaturalTransformation),
(Multiplication, NaturalTransformation),
(Comultiplication, NaturalTransformation),
(TwoCategory, HigherCategory),
(Bicategory, HigherCategory),
(Applicative, Endofunctor),
(Monad, Applicative),
(Comonad, Endofunctor),
(Monoid, Semigroup),
(MonoidalCategory, CategoryStructure),
(Product, Object),
(Coproduct, Object),
(Terminal, Object),
(InitialObject, Object),
(OppositeCategory, CategoryStructure),
(KleisliCategory, CategoryStructure),
(StateMonad, Monad),
(ReaderMonad, Monad),
(WriterMonad, Monad),
(FreeMonad, Monad),
(Representable, Functor),
(YonedaEmbedding, Functor),
(GaloisConnection, Adjunction),
(Interpretation, Functor),
(InstanceFunctor, Interpretation),
(SchemaCategory, CategoryStructure),
],
has_a: [
(Morphism, Source),
(Morphism, Target),
(Morphism, Kind),
(CategoryStructure, Object),
(CategoryStructure, Morphism),
(CategoryStructure, Composition),
(CategoryStructure, Identity),
(Adjunction, Unit),
(Adjunction, Counit),
(TwoCategory, CategoryStructure),
(TwoCategory, Functor),
(TwoCategory, NaturalTransformation),
(Applicative, Pure),
(Monad, Unit),
(Monad, Multiplication),
(Comonad, Counit),
(Comonad, Comultiplication),
(MonoidalCategory, Tensor),
(Monoid, Identity),
(Monoid, Multiplication),
(Algebra, StructureMap),
(Coalgebra, StructureMap),
(Interpretation, Syntactic),
(Interpretation, Semantic),
(InstanceFunctor, SchemaCategory),
],
opposes: [
(Algebra, Coalgebra),
(Coalgebra, Algebra),
(Monad, Comonad),
(Comonad, Monad),
(Product, Coproduct),
(Coproduct, Product),
(Terminal, InitialObject),
(InitialObject, Terminal),
(Unit, Counit),
(Counit, Unit),
(Syntactic, Semantic),
(Semantic, Syntactic),
],
}
#[derive(Debug, Clone)]
pub struct NoQuality;
impl crate::ontology::Quality for NoQuality {
type Individual = CategoryTheoryConcept;
type Value = ();
fn get(&self, _: &CategoryTheoryConcept) -> Option<()> {
None
}
}
impl Ontology for CategoryTheoryOntology {
type Cat = CategoryTheoryCategory;
type Qual = NoQuality;
fn axioms() -> Vec<Box<dyn Axiom>> {
crate::ontology::reasoning::structural_axioms_for::<Self::Cat>()
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::category::laws::assert_category_laws;
use crate::category::{Arrow, Category, FinitelyGenerated};
use proptest::prelude::*;
#[test]
fn category_theory_ontology_category_laws() {
assert_category_laws::<CategoryTheoryCategory>();
}
#[test]
fn category_theory_ontology_validates() {
CategoryTheoryOntology::validate()
.unwrap_or_else(|c| panic!("validation failed: {}", c.meta().description.as_str()));
}
#[test]
fn monad_is_applicative_is_endofunctor_is_functor() {
let sub: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Subsumption)
.map(|m| (m.source(), m.target()))
.collect();
assert!(sub.contains(&(
CategoryTheoryConcept::Monad,
CategoryTheoryConcept::Applicative
)));
assert!(sub.contains(&(
CategoryTheoryConcept::Applicative,
CategoryTheoryConcept::Endofunctor
)));
assert!(sub.contains(&(
CategoryTheoryConcept::Endofunctor,
CategoryTheoryConcept::Functor
)));
}
#[test]
fn monad_has_unit_and_multiplication() {
let parthood: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Parthood)
.map(|m| (m.source(), m.target()))
.collect();
assert!(parthood.contains(&(CategoryTheoryConcept::Monad, CategoryTheoryConcept::Unit)));
assert!(parthood.contains(&(
CategoryTheoryConcept::Monad,
CategoryTheoryConcept::Multiplication
)));
}
#[test]
fn specific_monads_are_monads() {
let sub: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Subsumption)
.map(|m| (m.source(), m.target()))
.collect();
for m in [
CategoryTheoryConcept::StateMonad,
CategoryTheoryConcept::ReaderMonad,
CategoryTheoryConcept::WriterMonad,
CategoryTheoryConcept::FreeMonad,
] {
assert!(
sub.contains(&(m, CategoryTheoryConcept::Monad)),
"{:?} should be-a Monad",
m
);
}
}
#[test]
fn algebra_opposes_coalgebra() {
let opp: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Opposition)
.map(|m| (m.source(), m.target()))
.collect();
assert!(opp.contains(&(
CategoryTheoryConcept::Algebra,
CategoryTheoryConcept::Coalgebra
)));
assert!(opp.contains(&(
CategoryTheoryConcept::Coalgebra,
CategoryTheoryConcept::Algebra
)));
}
#[test]
fn interpretation_is_functor_instance_specialises_interpretation() {
let sub: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Subsumption)
.map(|m| (m.source(), m.target()))
.collect();
assert!(sub.contains(&(
CategoryTheoryConcept::Interpretation,
CategoryTheoryConcept::Functor
)));
assert!(sub.contains(&(
CategoryTheoryConcept::InstanceFunctor,
CategoryTheoryConcept::Interpretation
)));
}
#[test]
fn interpretation_bridges_syntactic_and_semantic() {
let parthood: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Parthood)
.map(|m| (m.source(), m.target()))
.collect();
assert!(parthood.contains(&(
CategoryTheoryConcept::Interpretation,
CategoryTheoryConcept::Syntactic
)));
assert!(parthood.contains(&(
CategoryTheoryConcept::Interpretation,
CategoryTheoryConcept::Semantic
)));
let opp: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Opposition)
.map(|m| (m.source(), m.target()))
.collect();
assert!(opp.contains(&(
CategoryTheoryConcept::Syntactic,
CategoryTheoryConcept::Semantic
)));
}
#[test]
fn galois_connection_is_adjunction() {
let sub: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Subsumption)
.map(|m| (m.source(), m.target()))
.collect();
assert!(sub.contains(&(
CategoryTheoryConcept::GaloisConnection,
CategoryTheoryConcept::Adjunction
)));
}
proptest! {
#[test]
fn prop_every_arrow_is_named(_seed in any::<u32>()) {
for m in CategoryTheoryCategory::morphisms() {
prop_assert!(!m.meta().name.as_str().is_empty());
}
}
#[test]
fn prop_subsumption_targets_valid(_seed in any::<u32>()) {
let variants: Vec<_> = CategoryTheoryConcept::variants();
for m in CategoryTheoryCategory::morphisms() {
if m.kind() == CategoryTheoryRelationKind::Subsumption {
prop_assert!(variants.contains(&m.source()));
prop_assert!(variants.contains(&m.target()));
}
}
}
#[test]
fn prop_structural_axioms_hold(_seed in any::<u32>()) {
for axiom in CategoryTheoryOntology::axioms() {
match axiom.verify() {
Ok(_) => {}
Err(c) => prop_assert!(
false,
"structural axiom failed: {}",
c.meta().name.as_str()
),
}
}
}
#[test]
fn prop_opposition_symmetric(_seed in any::<u32>()) {
let opp: Vec<_> = CategoryTheoryCategory::morphisms()
.iter()
.filter(|m| m.kind() == CategoryTheoryRelationKind::Opposition)
.map(|m| (m.source(), m.target()))
.collect();
for (a, b) in &opp {
prop_assert!(
opp.contains(&(*b, *a)),
"opposition ({:?}, {:?}) missing symmetric partner",
a, b
);
}
}
#[test]
fn prop_concept_count_is_sufficient(_seed in any::<u32>()) {
let variants: Vec<_> = CategoryTheoryConcept::variants();
prop_assert!(variants.len() >= 40,
"expected >= 40 concepts after extension, got {}", variants.len());
}
}
}