diff --git a/unified.md b/unified.md index f7d1019..553a1da 100644 --- a/unified.md +++ b/unified.md @@ -2,44 +2,44 @@ 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| +| **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