Topoi

; Monomorphism: injective function (cancellable on the left).
; m is mono if m(g(x)) = m(g'(x)) for all x implies g = g'.
; In Set, mono = injective.

(define (mono? f domain)
  ; Check: no two distinct inputs map to the same output
  (let loop ((remaining domain) (seen '()))
    (if (null? remaining) #t
        (let ((val (f (car remaining))))
          (if (member val seen) #f
              (loop (cdr remaining) (cons val seen)))))))

; Injective: include even numbers into all naturals
(define (include-evens x) x)  ; identity on evens
(display "include-evens mono? ")
(display (mono? include-evens '(0 2 4 6 8))) (newline)

; Not injective: mod 3
(define (mod3 x) (modulo x 3))
(display "mod3 mono? ")
(display (mono? mod3 '(0 1 2 3 4 5))) (newline)

; Subobject: the equivalence class of monos.
; (0,2,4) ↪ (0,1,2,3,4) and (0,2,4) ↪ (0,1,2,3,4)
; via different injections define the SAME subobject
; if they have the same image.

; Subobject classifier in Set:
; Ω = (#t, #f)
; true : 1 -> Ω sends () to #t
;
; For every subset A ⊆ B, the characteristic function
; χ : B -> Ω sends x to #t if x ∈ A, #f otherwise.
;
; The pullback of true along χ recovers A.

(define omega '(#t #f))

; true : 1 -> Ω
(define (true-arrow _) #t)

; Characteristic function for a subset
(define (char-fn subset)
  (lambda (x) (if (member x subset) #t #f)))

; Example: B = (1,2,3,4,5), A = (2,4)
(define B '(1 2 3 4 5))
(define A '(2 4))

(define chi (char-fn A))

(display "χ(1)=") (display (chi 1))
(display " χ(2)=") (display (chi 2))
(display " χ(3)=") (display (chi 3))
(display " χ(4)=") (display (chi 4))
(display " χ(5)=") (display (chi 5)) (newline)

; Pullback: recover A as (x in B where χ(x) = true)
(define (pullback-of-true chi domain)
  (filter chi domain))

(display "pullback recovers A: ")
(display (pullback-of-true chi B))
; => (2 4)

; The topos checklist for Set:
;
; 1. Cartesian closed?
;    - Terminal object: the one-element set (*)
;    - Products: A × B (cartesian product)
;    - Exponentials: B^A (function set)   ✓
;
; 2. All finite limits?
;    - Equalizers: (x in A where f(x) = g(x))
;    - Pullbacks: from products + equalizers   ✓
;
; 3. Subobject classifier?
;    - Ω = (#t, #f), true : 1 -> Ω   ✓

; Let's verify the equalizer in Set:
(define (equalizer f g domain)
  (filter (lambda (x) (equal? (f x) (g x))) domain))

(define (f x) (* x x))     ; x²
(define (g x) (+ (* 2 x) 3))  ; 2x + 3

(display "equalizer of x² and 2x+3 over 0..5: ")
(display (equalizer f g '(0 1 2 3 4 5))) (newline)
; => (3)  because 9 = 9

; Pullback via equalizer of products:
; Given f: A -> C and g: B -> C,
; pullback = ((a,b) in A×B where f(a) = g(b))
(define (pullback f g domA domB)
  (let loop ((as domA) (result '()))
    (if (null? as) (reverse result)
        (let inner ((bs domB) (acc result))
          (if (null? bs) (loop (cdr as) acc)
              (if (equal? (f (car as)) (g (car bs)))
                  (inner (cdr bs) (cons (cons (car as) (car bs)) acc))
                  (inner (cdr bs) acc)))))))

(display "pullback f(a)=g(b): ")
(display (pullback f g '(0 1 2 3 4 5) '(0 1 2 3 4 5)))
; pairs (a,b) where a² = 2b+3

; Multi-valued truth in a small presheaf category.
;
; Category C: two objects (a, b) with one non-identity arrow f: a -> b.
; A presheaf is a functor C^op -> Set.
;
; Ω(b) = sieves on b = downward-closed sets of arrows into b
;   - maximal sieve: (id_b, f)  (all arrows into b)
;   - sieve (f)                 (only the arrow from a)
;   - empty sieve: ()
;
; So Ω(b) has THREE elements, not two!

(define omega-at-b
  '((max-sieve . (id-b f))    ; totally true
    (partial   . (f))          ; true at stage a only
    (empty     . ())))          ; false

(display "Ω(b) has ") (display (length omega-at-b))
(display " truth values:") (newline)
(for-each (lambda (s)
  (display "  ") (display (car s))
  (display " = (") (display (cdr s))
  (display ")") (newline))
  omega-at-b)

; Ω(a) = sieves on a = (id_a) or ()
; Only two truth values at stage a (no arrows in except id).
(define omega-at-a
  '((max-sieve . (id-a))
    (empty     . ())))

(display "Ω(a) has ") (display (length omega-at-a))
(display " truth values") (newline)

; The "partial" truth value has no classical equivalent.
; ¬partial ≠ partial, but partial ∨ ¬partial ≠ max-sieve.
; Excluded middle fails. Logic is intuitionistic.
(display "Excluded middle fails: partial ∨ ¬partial ≠ true")

; Intuitionistic logic: Heyting algebra on Ω.
;
; In Set (classical): Ω = (set #t #f), Boolean algebra.
; In a topos: Ω is a Heyting algebra.
;
; Heyting algebra operations:
;   ∧ (meet)  = product  = AND
;   ∨ (join)  = coproduct = OR
;   → (impl)  = exponential = implies
;   ¬p = p → false
;
; Key difference from Boolean algebra:
;   ¬¬p does NOT imply p.

; Heyting algebra on (false, partial, true) (linearly ordered)
(define (h-and a b) (min a b))
(define (h-or a b) (max a b))
(define (h-implies a b) (if (<= a b) 2 b))  ; 2=true, 1=partial, 0=false
(define (h-not a) (h-implies a 0))

(define truth-vals '((false . 0) (partial . 1) (true . 2)))

; ¬partial = partial → false
(display "¬partial = ") (display (h-not 1)) (newline)
; => 0 (false)

; ¬¬partial = ¬false = false → false
(display "¬¬partial = ") (display (h-not (h-not 1))) (newline)
; => 2 (true)

; But partial ≠ true!
(display "partial = ") (display 1) (newline)
(display "¬¬partial ≠ partial: double negation fails") (newline)

; Excluded middle: p ∨ ¬p
(display "partial ∨ ¬partial = ")
(display (h-or 1 (h-not 1))) (newline)
; => 1 (partial), not 2 (true). Excluded middle fails!

; In Boolean algebra: ¬partial would be true, giving p ∨ ¬p = true.
; Heyting algebra is strictly weaker.