Calculating Intuitionistic Logic in Scala
summary
A working Scala library takes a finite category, builds the topos of diagrams (presheaves) over it, and computes Ω (subobject classifier) by enumerating compatible subobjects of representable functors; code shows how to build representables, classify inclusions, and implement conjunction, disjunction, implication and negation. Tests run against examples (natural-number timelines, parallel pair, finite sets) and validate logical laws. Implementation leans on path-dependent types, macros and lazy vals, and is pragmatic about enumeration limits; the examples and unit tests demonstrate the approach actually computes and checks results.
AI-written summary · about
chapters (25)
- 0:00Intro
- 2:55What is a graph
- 5:08Not enumerable sets
- 6:13Categories
- 7:49Defining Categories
- 9:35Natural Numbers
- 11:04Set Category
- 12:30Set Function
- 13:18Setmorphism
- 13:31Factor
- 15:24Constant Factor
- 17:39Natural Transformation
- 20:35Preshift
- 22:44Diagrams in Sets
- 24:59Diagram over Natural Numbers
- 26:43Transitions
- 32:24Tapas
- 34:05Parallel Pair
- 34:52Sub Object Classifier
- 36:14Omega
- 37:57Representation
- 39:26Union Dilemma
- 51:27Predicate
- 52:55Unit Tests
- 54:25Conclusion
related talks
32mClassical Category Theory in Plain Scala
53mIntroduction to Intuitionistic Type Theory
52mWhat logic can teach us, Scala programmers
41mA Pragmatic Introduction to Category Theory
49mCompile-time Logic Programming in Scala: what for?
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
40mA Pragmatic Introduction to Category Theories
30mDisplayed Monoidal Categories for the Semantics of Linear Logic