1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
//! Kind-tags for arrows at every cell-level of Cat (issue #153).
//!
//! Per Gruber (1993) KAS 5 — "ontology = formally-named relations" —
//! every arrow in pr4xis carries a relation-kind tag. At 1-cell level
//! this is `RelationKind` (Subsumption, Parthood, etc. from the
//! Relations ontology). At the 1-cells-in-Cat, 2-cells-in-Cat, and
//! structured-2-cell-pair levels, we need analogous kind enums.
//!
//! References:
//! - Mac Lane (1971) *Categories for the Working Mathematician* I.3, IV.1, I.4
//! - Awodey (2010) *Category Theory* §7, §9
//! - Smith et al. (2005) OBO Relation Ontology (principle: every
//! relation has a canonical named type)
/// Classification of a functor F: C → D (Mac Lane 1971 I.3; Awodey §7.2).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum FunctorKind {
/// Injective on each Hom-set: F: Hom(A,B) → Hom(F A, F B) is injective.
Faithful,
/// Surjective on each Hom-set.
Full,
/// Both faithful and full — the strongest "embedding" classification.
FullyFaithful,
/// Discards structure (e.g., Group → Set, forgetting the group operation).
Forgetful,
/// Left adjoint to a forgetful functor (Mac Lane IV.1 free-forgetful paradigm).
Free,
/// Trivial self-functor `Id_C: C → C`.
Identity,
/// `Hom(A, -): C → Set` for some fixed A — the Yoneda-representable functor.
Representable,
/// Inclusion functor from a subcategory.
Inclusion,
/// Not further classified.
Generic,
}
/// Classification of a natural transformation η: F ⇒ G
/// (Mac Lane 1971 I.4; Awodey §7.5).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum NatTransKind {
/// Every component η_A is iso in the target category.
NaturalIsomorphism,
/// Every component η_A is a monomorphism.
NaturalMonomorphism,
/// Every component η_A is an epimorphism.
NaturalEpimorphism,
/// The canonical unit η: Id_C ⇒ G∘F of an adjunction.
AdjunctionUnit,
/// The canonical counit ε: F∘G ⇒ Id_D of an adjunction.
AdjunctionCounit,
/// Not further classified.
Generic,
}
/// Classification of an adjunction F ⊣ G
/// (Mac Lane 1971 IV.3; Awodey §9.5).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum AdjunctionKind {
/// Unit η is a natural isomorphism — C embeds as reflective subcategory of D.
Reflection,
/// Counit ε is a natural isomorphism — D embeds as coreflective subcategory of C.
Coreflection,
/// Both unit and counit are natural isos — C and D are categorically equivalent.
Equivalence,
/// Free-forgetful paradigm: F constructs the free object, G forgets structure.
FreeForgetful,
/// Not further classified.
Generic,
}