|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) 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|
In combinatory logic?, in the λ-calculus, or more generally in type theory, a looping combinator? is closely akin to a fixed-point combinator, but rather than producing a true fixed point, it produces a sequence of points each of which is the image of the next.
where is a looping combinator.
This is a coinductive definition. Unraveled explicitly, it means that a looping combinator comes with a sequence of combinators for and reductions
Per Martin-Löf’s original dependent type theory, which had the additional rule , was shown to be inconsistent by Girard's paradox. In the 1980’s, Meyer, Reinhold, and Howe (see references) showed that this paradox could be modified to construct a looping combinator.
In the short paper
it was claimed that from Girard’s paradox one could actually construct a fixed-point combinator. The proof turned out to be flawed, but it was sufficient to produce a looping combinator. Details can be found in
Mark Reinhold, “Typechecking is Undecidable When ‘Type’ is a Type”, 1989, citeseer
Douglas Howe, “The Computational Behaviour of Girard’s Paradox”, Cornell University Technical Report, 1987, link.