pr4xis 0.6.0

Prove your domain is correct — ontology-driven rule enforcement with category theory, logical composition, and runtime state machines
Documentation 
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

use super::category::Category;
use super::functor::Functor;

// Adjunction — a pair of functors that are "optimally inverse."
//
// Given categories C and D, an adjunction F ⊣ G consists of:
// - Left adjoint F: C → D (the "free" functor)
// - Right adjoint G: D → C (the "forgetful" functor)
//
// The defining property: for all objects A in C and B in D,
//   Hom_D(F(A), B) ≅ Hom_C(A, G(B))
//
// This natural bijection means: a morphism F(A) → B in D
// corresponds uniquely to a morphism A → G(B) in C.
//
// Adjunctions are everywhere in praxis:
// - Parse ⊣ Generate — parsing text to semantics, generating text from semantics
// - Channel ⊣ Decode — noisy channel corruption, Bayesian correction
// - Abstract ⊣ Concretize — moving between abstraction levels
// - Forget ⊣ Free — forgetting structure, freely generating structure
//
// The unit η: Id_C → G∘F and counit ε: F∘G → Id_D capture the
// information loss: G∘F ≠ Id (you can't perfectly recover from
// the round trip), but η and ε are the "best approximation."
//
// References:
// - Mac Lane, Categories for the Working Mathematician (1971), Ch. IV
// - Awodey, Category Theory (2010), Ch. 9
// - Lambek & Scott, Introduction to Higher Order Categorical Logic (1986)

/// An adjunction F ⊣ G between two categories.
///
/// F is the left adjoint (free construction / forward transform).
/// G is the right adjoint (forgetful / inverse transform).
///
/// The unit η: Id → G∘F captures what is preserved by the round trip.
/// The counit ε: F∘G → Id captures what is lost.
pub trait Adjunction {
    /// The left adjoint functor F: C → D.
    type Left: Functor;
    /// The right adjoint functor G: D → C.
    type Right: Functor<Source = <Self::Left as Functor>::Target, Target = <Self::Left as Functor>::Source>;

    /// The unit component at an object A in C.
    ///
    /// η_A: A → G(F(A))
    ///
    /// Embeds A into the round-trip G∘F. If η is an isomorphism,
    /// the adjunction is a reflection (no information loss on C's side).
    fn unit(
        obj: &<<Self::Left as Functor>::Source as Category>::Object,
    ) -> <<Self::Left as Functor>::Source as Category>::Morphism;

    /// The counit component at an object B in D.
    ///
    /// ε_B: F(G(B)) → B
    ///
    /// Projects the round-trip F∘G back to B. If ε is an isomorphism,
    /// the adjunction is a coreflection (no information loss on D's side).
    fn counit(
        obj: &<<Self::Left as Functor>::Target as Category>::Object,
    ) -> <<Self::Left as Functor>::Target as Category>::Morphism;
}