Enriched Categories

; An ordinary category has hom-SETS: finite collections of morphisms.
; An enriched category has hom-OBJECTS from some monoidal category V.
;
; V must provide:
;   - a tensor product (⊗) to combine hom-objects
;   - a unit object (I) to source identity morphisms
;
; We'll build three examples:
;   1. V = Bool  (hom = true/false)    => preorders
;   2. V = [0,∞] (hom = distance)      => metric spaces
;   3. V = Set   (hom = set)           => ordinary categories

; First: a monoidal category is (objects, tensor, unit)
(define (make-monoidal tensor unit)
  (list tensor unit))

(define (monoidal-tensor m) (car m))
(define (monoidal-unit m) (cadr m))

; Bool as a monoidal category: tensor = AND, unit = #t
(define bool-monoidal (make-monoidal (lambda (a b) (and a b)) #t))

(display "Bool tensor: #t ⊗ #t = ")
(display ((monoidal-tensor bool-monoidal) #t #t)) (newline)
(display "Bool tensor: #t ⊗ #f = ")
(display ((monoidal-tensor bool-monoidal) #t #f)) (newline)
(display "Bool unit: ")
(display (monoidal-unit bool-monoidal))

; A Bool-enriched category is a preorder.
; hom(a,b) = #t means a ≤ b, #f means not.
; Composition: hom(b,c) AND hom(a,b) => hom(a,c)  [transitivity]
; Identity: true => hom(a,a)                       [reflexivity]

(define (make-preorder leq?)
  (list 'preorder leq?))

(define (preorder-hom p a b)
  ((cadr p) a b))

; The enriched composition law: if a≤b and b≤c then a≤c
(define (preorder-compose p a b c)
  (and (preorder-hom p a b)
       (preorder-hom p b c)))

; Example: divisibility preorder on positive integers
; a ≤ b iff a divides b
(define divides-preorder
  (make-preorder (lambda (a b) (= 0 (modulo b a)))))

; Check hom-objects (true/false)
(display "hom(2,6) = ") (display (preorder-hom divides-preorder 2 6)) (newline)
(display "hom(3,6) = ") (display (preorder-hom divides-preorder 3 6)) (newline)
(display "hom(4,6) = ") (display (preorder-hom divides-preorder 4 6)) (newline)

; Verify composition = transitivity: 2|6 and 6|12 => 2|12
(display "compose(2,6,12) = ")
(display (preorder-compose divides-preorder 2 6 12)) (newline)

; Verify identity = reflexivity: hom(a,a) = #t
(display "hom(5,5) = ") (display (preorder-hom divides-preorder 5 5)) (newline)

; This IS the enriched category. No extra axioms needed.
; The monoidal structure of Bool enforces preorder laws.

; A [0,∞]-enriched category is a (generalized) metric space.
; hom(a,b) = distance from a to b
; Tensor = +, unit = 0
;
; Composition law: hom(a,b) + hom(b,c) >= hom(a,c)
;   This IS the triangle inequality.
; Identity law: 0 >= hom(a,a)
;   So hom(a,a) = 0. Self-distance is zero.

(define (make-metric dist)
  (list 'metric dist))

(define (metric-hom m a b)
  ((cadr m) a b))

; Check the enriched composition law (triangle inequality)
(define (metric-composition-ok? m a b c)
  (>= (+ (metric-hom m a b) (metric-hom m b c))
      (metric-hom m a c)))

; Example: points on the real line
(define real-line
  (make-metric (lambda (a b) (abs (- a b)))))

(display "hom(1, 4) = ") (display (metric-hom real-line 1 4)) (newline)
(display "hom(4, 10) = ") (display (metric-hom real-line 4 10)) (newline)
(display "hom(1, 10) = ") (display (metric-hom real-line 1 10)) (newline)

; Triangle inequality: d(1,4) + d(4,10) >= d(1,10)
; 3 + 6 >= 9 ✓
(display "triangle(1,4,10)? ")
(display (metric-composition-ok? real-line 1 4 10)) (newline)

; Identity: d(a,a) = 0
(display "hom(7,7) = ") (display (metric-hom real-line 7 7)) (newline)

; A tighter example: d(0,3) + d(3,5) = 3+2 = 5 >= d(0,5) = 5
(display "triangle(0,3,5)? ")
(display (metric-composition-ok? real-line 0 3 5))
; Equality holds — the shortest path goes through the midpoint.

; Unified enriched composition check.
; Given a monoidal category V and a hom-function,
; verify the composition law:
;   tensor(hom(b,c), hom(a,b)) => hom(a,c)
;
; For Bool: AND(hom(b,c), hom(a,b)) implies hom(a,c)
; For [0,∞]: hom(a,b) + hom(b,c) >= hom(a,c)

; Bool version: composition = implication
(define (bool-compose-ok? hom a b c)
  ; If hom(a,b) AND hom(b,c), then hom(a,c) must hold
  (if (and (hom a b) (hom b c))
      (hom a c)    ; must be #t
      #t))         ; vacuously true

; Metric version: composition = triangle inequality
(define (metric-compose-ok? hom a b c)
  (>= (+ (hom a b) (hom b c))
      (hom a c)))

; Test Bool (divisibility)
(define (divides? a b) (= 0 (modulo b a)))

(display "Bool composition checks (divisibility):
")
(display "  2|6 and 6|12 => 2|12? ")
(display (bool-compose-ok? divides? 2 6 12)) (newline)
(display "  3|6 and 6|18 => 3|18? ")
(display (bool-compose-ok? divides? 3 6 18)) (newline)

; Test metric (real line)
(define (real-dist a b) (abs (- a b)))

(display "
Metric composition checks (triangle inequality):
")
(display "  d(0,3)+d(3,7) >= d(0,7)? ")
(display (metric-compose-ok? real-dist 0 3 7)) (newline)
(display "  3 + 4 = 7 >= 7 ✓
")

; 2D Euclidean distance — triangle inequality is strict
(define (dist-2d p q)
  (sqrt (+ (expt (- (car p) (car q)) 2)
           (expt (- (cdr p) (cdr q)) 2))))

(define A (cons 0 0))
(define B (cons 3 0))
(define C (cons 3 4))

(display "
2D triangle inequality:
")
(display "  d(A,B) = ") (display (dist-2d A B)) (newline)
(display "  d(B,C) = ") (display (dist-2d B C)) (newline)
(display "  d(A,C) = ") (display (dist-2d A C)) (newline)
(display "  3 + 4 = 7 >= 5? ")
(display (metric-compose-ok? dist-2d A B C))
; Strict inequality: going through B is longer than the direct path.

; Cat-enriched category = 2-category.
; hom(A,B) is a CATEGORY, not a set.
;   Objects of hom(A,B) = functors A -> B (1-morphisms)
;   Morphisms of hom(A,B) = natural transformations (2-morphisms)
;
; We can't build full functor categories in Scheme,
; but we can model the structure: hom-objects that are
; themselves categories with vertical composition.

; A 2-cell: a natural transformation between two functors
(define (make-2-cell name source target component)
  (list name source target component))

(define (two-cell-name nt) (car nt))
(define (two-cell-source nt) (cadr nt))
(define (two-cell-target nt) (caddr nt))
(define (two-cell-at nt x) ((cadddr nt) x))

; Vertical composition of 2-cells (within a hom-category)
; If α : F => G and β : G => H, then β∘α : F => H
(define (vertical-compose beta alpha)
  (make-2-cell
    (string-append (two-cell-name beta) "." (two-cell-name alpha))
    (two-cell-source alpha)
    (two-cell-target beta)
    (lambda (x) (list 'compose (two-cell-at beta x) (two-cell-at alpha x)))))

; Example: three "functors" (just named mappings for illustration)
; F: x -> x+1, G: x -> x+2, H: x -> x+3
; α : F => G  (component at x: the morphism x+1 -> x+2)
; β : G => H  (component at x: the morphism x+2 -> x+3)

(define alpha
  (make-2-cell "α" 'F 'G (lambda (x) (list '-> (+ x 1) (+ x 2)))))

(define beta
  (make-2-cell "β" 'G 'H (lambda (x) (list '-> (+ x 2) (+ x 3)))))

(define beta-alpha (vertical-compose beta alpha))

(display "α at 5: ") (display (two-cell-at alpha 5)) (newline)
(display "β at 5: ") (display (two-cell-at beta 5)) (newline)
(display "β∘α at 5: ") (display (two-cell-at beta-alpha 5)) (newline)
(display "β∘α source: ") (display (two-cell-source beta-alpha)) (newline)
(display "β∘α target: ") (display (two-cell-target beta-alpha))
; The hom-category hom(A,B) has its own composition. That's 2-categorical.

; Set enriched over Set = ordinary category.
; The internal hom [a,b] is the set of functions a -> b.
; Composition: [b,c] × [a,b] -> [a,c]
;   is just ordinary function composition.

; Model: finite sets as lists, functions as association lists
(define (make-fn domain mapping)
  (list domain mapping))

(define (apply-fn f x)
  (let ((pair (assoc x (cadr f))))
    (if pair (cdr pair) 'undefined)))

; Two functions to compose
(define f (make-fn '(1 2 3) '((1 . a) (2 . b) (3 . c))))
(define g (make-fn '(a b c) '((a . x) (b . y) (c . z))))

; Enriched composition: build the composite function
(define (compose-fn g f)
  (make-fn
    (car f)
    (map (lambda (pair)
           (cons (car pair) (apply-fn g (cdr pair))))
         (cadr f))))

(define gf (compose-fn g f))

(display "f(1)=") (display (apply-fn f 1))
(display ", g(a)=") (display (apply-fn g 'a))
(display ", (g∘f)(1)=") (display (apply-fn gf 1)) (newline)

(display "f(2)=") (display (apply-fn f 2))
(display ", g(b)=") (display (apply-fn g 'b))
(display ", (g∘f)(2)=") (display (apply-fn gf 2)) (newline)

; The enriched identity: unit I -> [a,a] picks out id_a
(define (enriched-id domain)
  (make-fn domain (map (lambda (x) (cons x x)) domain)))

(define id-123 (enriched-id '(1 2 3)))
(display "id(1)=") (display (apply-fn id-123 1))
(display ", id(2)=") (display (apply-fn id-123 2))
; Self-enrichment makes the internal structure explicit.