Taken from 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 |