adding curry-howard-lambek table

README.md

@@ -293,6 +293,7 @@ There is simply no way around this. Abstract thinking *HAS TO BE LEARNED.* And I
   - obeys rules,
   - is built gradually from earlier stages,
   - offers strict guarantees (invariants).
+- Stratification, predicativity
 
 ## The many joys of world building
 
@@ -354,6 +355,12 @@ There is simply no way around this. Abstract thinking *HAS TO BE LEARNED.* And I
 
 [Link to the Meta thinking section](meta.md)
 
+### Unified theory of everything
+
+- Different fields are deeply connected.
+
+[Link to the Deep Connections section](unified.md)
+
 ## Problem solving
 
 [Link to the Problem Solving section](solve.md)

unified.md

@@ -0,0 +1,46 @@
+# Unified theory
+
+Taken from [Computational Trilogy](https://ncatlab.org/nlab/show/computational+trilogy), it's actually more of a quadrilogy (or tetralogy).
+
+| logic | set theory | category theory | type theory |
+|:-----:|:----------:|:---------------:|:-----------:|
+| proposition | set | object| type|
+| predicate| family of sets| display morphism| dependent type|
+| proof| element| generalized element| term/program|
+| cut rule || composition of classifying morphisms / pullback of display maps | substitution|
+| introduction rule for implication|| counit for hom-tensor adjunction| lambda |
+| elimination rule for implication || unit for hom-tensor adjunction| application|
+| cut elimination for implication|| one of the zigzag identities for hom-tensor adjunction| beta reduction|
+| identity elimination for implication || the other zigzag identity for hom-tensor adjunction | eta conversion|
+| true | singleton | terminal object/(-2)-truncated object| h-level 0-type/unit type|
+| false| empty set | initial object| empty type |
+| proposition, truth value | subsingleton| subterminal object/(-1)-truncated object| h-proposition, mere proposition|
+| logical conjunction | cartesian product| product | product type|
+| disjunction| disjoint union (support of)| coproduct ((-1)-truncation of)| sum type (bracket type of)|
+| implication| function set (into subsingleton)| internal hom (into subterminal object)| function type (into h-proposition)|
+| negation | function set into empty set| internal hom into initial object| function type into empty type |
+| universal quantification | indexed cartesian product (of family of subsingletons) | dependent product (of family of subterminal objects)| dependent product type (of family of h-propositions)|
+| existential quantification| indexed disjoint union (support of)| dependent sum ((-1)-truncation of)| dependent sum type (bracket type of)|
+| logical equivalence | bijection set | object of isomorphisms | equivalence type|
+|| support set| support object/(-1)-truncation| propositional truncation/bracket type |
+||| n-image of morphism into terminal object/n-truncation| n-truncation modality|
+| equality | diagonal function/diagonal subset/diagonal relation| path space object| identity type/path type |
+| completely presented set | set| discrete object/0-truncated object| h-level 2-type/set/h-set|
+| set| set with equivalence relation| internal 0-groupoid| Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation |
+|| equivalence class/quotient set | quotient| quotient type |
+| induction|| colimit | inductive type, W-type, M-type|
+| higher induction|| higher colimit| higher inductive type|
+| -|| 0-truncated higher colimit| quotient inductive type |
+| coinduction|| limit | coinductive type|
+|| preset || type without identity types |
+|| set of truth values| subobject classifier| type of propositions|
+| domain of discourse | universe| object classifier| type universe |
+| modality || closure operator, (idempotent) monad| modal type theory, monad (in computer science)|
+| linear logic || (symmetric, closed) monoidal category| linear type theory/quantum computation|
+| proof net|| string diagram| quantum circuit |
+| (absence of) contraction rule|| (absence of) diagonal| no-cloning theorem|
+||| synthetic mathematics| domain specific embedded programming language|
+
+## Work in progress
+
+[Back to Elements](README.md#unified-theory-of-everything)