Skip to content

Commit a707d2f

Browse files
spamegg1spamegg1
committed
fixing unified table
1 parent f806247 commit a707d2f

File tree

1 file changed

+38
-38
lines changed

1 file changed

+38
-38
lines changed

‎unified.md

Lines changed: 38 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -2,44 +2,44 @@
22

33
Taken from [Computational Trilogy](https://ncatlab.org/nlab/show/computational+trilogy), it's actually more of a quadrilogy (or tetralogy).
44

5-
| logic | set theory | category theory | type theory |
6-
|:-----:|:----------:|:---------------:|:-----------:|
7-
| proposition | set | object| type|
8-
| predicate| family of sets| display morphism| dependent type|
9-
| proof| element| generalized element| term/program|
10-
| cut rule || composition of classifying morphisms / pullback of display maps | substitution|
11-
| introduction rule for implication|| counit for hom-tensor adjunction| lambda |
12-
| elimination rule for implication || unit for hom-tensor adjunction| application|
13-
| cut elimination for implication|| one of the zigzag identities for hom-tensor adjunction| beta reduction|
14-
| identity elimination for implication || the other zigzag identity for hom-tensor adjunction | eta conversion|
15-
| true | singleton | terminal object/(-2)-truncated object| h-level 0-type/unit type|
16-
| false| empty set | initial object| empty type |
17-
| proposition, truth value | subsingleton| subterminal object/(-1)-truncated object| h-proposition, mere proposition|
18-
| logical conjunction | cartesian product| product | product type|
19-
| disjunction| disjoint union (support of)| coproduct ((-1)-truncation of)| sum type (bracket type of)|
20-
| implication| function set (into subsingleton)| internal hom (into subterminal object)| function type (into h-proposition)|
21-
| negation | function set into empty set| internal hom into initial object| function type into empty type |
22-
| universal quantification | indexed cartesian product (of family of subsingletons) | dependent product (of family of subterminal objects)| dependent product type (of family of h-propositions)|
23-
| existential quantification| indexed disjoint union (support of)| dependent sum ((-1)-truncation of)| dependent sum type (bracket type of)|
24-
| logical equivalence | bijection set | object of isomorphisms | equivalence type|
25-
|| support set| support object/(-1)-truncation| propositional truncation/bracket type |
26-
||| n-image of morphism into terminal object/n-truncation| n-truncation modality|
27-
| equality | diagonal function/diagonal subset/diagonal relation| path space object| identity type/path type |
28-
| completely presented set | set| discrete object/0-truncated object| h-level 2-type/set/h-set|
29-
| set| set with equivalence relation| internal 0-groupoid| Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation |
30-
|| equivalence class/quotient set | quotient| quotient type |
31-
| induction|| colimit | inductive type, W-type, M-type|
32-
| higher induction|| higher colimit| higher inductive type|
33-
| -|| 0-truncated higher colimit| quotient inductive type |
34-
| coinduction|| limit | coinductive type|
35-
|| preset || type without identity types |
36-
|| set of truth values| subobject classifier| type of propositions|
37-
| domain of discourse | universe| object classifier| type universe |
38-
| modality || closure operator, (idempotent) monad| modal type theory, monad (in computer science)|
39-
| linear logic || (symmetric, closed) monoidal category| linear type theory/quantum computation|
40-
| proof net|| string diagram| quantum circuit |
41-
| (absence of) contraction rule|| (absence of) diagonal| no-cloning theorem|
42-
||| synthetic mathematics| domain specific embedded programming language|
5+
| **logic** | **set theory** | **category theory** | **type theory** |
6+
|--------------------------------------|--------------------------------------------------------|-----------------------------------------------------------------|---------------------------------------------------------------------------------------|
7+
| proposition | set | object | type |
8+
| predicate | family of sets | display morphism | dependent type |
9+
| proof | element | generalized element | term/program |
10+
| cut rule | | composition of classifying morphisms / pullback of display maps | substitution |
11+
| introduction rule for implication | | counit for hom-tensor adjunction | lambda |
12+
| elimination rule for implication | | unit for hom-tensor adjunction | application |
13+
| cut elimination for implication | | one of the zigzag identities for hom-tensor adjunction | beta reduction |
14+
| identity elimination for implication | | the other zigzag identity for hom-tensor adjunction | eta conversion |
15+
| true | singleton | terminal object/(-2)-truncated object | h-level 0-type/unit type |
16+
| false | empty set | initial object | empty type |
17+
| proposition, truth value | subsingleton | subterminal object/(-1)-truncated object | h-proposition, mere proposition |
18+
| logical conjunction | cartesian product | product | product type |
19+
| disjunction | disjoint union (support of) | coproduct ((-1)-truncation of) | sum type (bracket type of) |
20+
| implication | function set (into subsingleton) | internal hom (into subterminal object) | function type (into h-proposition) |
21+
| negation | function set into empty set | internal hom into initial object | function type into empty type |
22+
| universal quantification | indexed cartesian product (of family of subsingletons) | dependent product (of family of subterminal objects) | dependent product type (of family of h-propositions) |
23+
| existential quantification | indexed disjoint union (support of) | dependent sum ((-1)-truncation of) | dependent sum type (bracket type of) |
24+
| logical equivalence | bijection set | object of isomorphisms | equivalence type |
25+
| | support set | support object/(-1)-truncation | propositional truncation/bracket type |
26+
| | | n-image of morphism into terminal object/n-truncation | n-truncation modality |
27+
| equality | diagonal function/diagonal subset/diagonal relation | path space object | identity type/path type |
28+
| completely presented set | set | discrete object/0-truncated object | h-level 2-type/set/h-set |
29+
| set | set with equivalence relation | internal 0-groupoid | Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation |
30+
| | equivalence class/quotient set | quotient | quotient type |
31+
| induction | | colimit | inductive type, W-type, M-type |
32+
| higher induction | | higher colimit | higher inductive type |
33+
| - | | 0-truncated higher colimit | quotient inductive type |
34+
| coinduction | | limit | coinductive type |
35+
| | preset | | type without identity types |
36+
| | set of truth values | subobject classifier | type of propositions |
37+
| domain of discourse | universe | object classifier | type universe |
38+
| modality | | closure operator, (idempotent) monad | modal type theory, monad (in computer science) |
39+
| linear logic | | (symmetric, closed) monoidal category | linear type theory/quantum computation |
40+
| proof net | | string diagram | quantum circuit |
41+
| (absence of) contraction rule | | (absence of) diagonal | no-cloning theorem |
42+
| | | synthetic mathematics | domain specific embedded programming language |
4343

4444
## Work in progress
4545

0 commit comments

Comments
 (0)