**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

**homotopy theory, (∞,1)-category theory, homotopy type theory**

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…

models: topological, simplicial, localic, …

see also **algebraic topology**

**Introductions**

**Definitions**

**Paths and cylinders**

**Homotopy groups**

**Basic facts**

**Theorems**

In intuitionistic type theory the perspective of propositions as types identifies mere propositions with (speaking in categorical semantics) monomorphisms into the given context type. If one instead considers linear type theory then it makes sense to consider those propositions, in this sense, which come from monomorphisms that are split monomorphisms, hence those for which there is a projection from the context to the subobject that represents the proposition. For these one might speak of “propositions as projections”.

For instance in a category of Hilbert spaces, regarded as semantics for bare multiplicative linear type theory, then projections correspond to (closed) linear subspaces. These are just the propositions in the corresponding quantum logic. If we regard a proposition *as* its corresponding projection, then it is natural to consider it also as being the *application* of this projection, in that the truth of the proposition is thought of as the image of applying this projection. In terms of quantum physics this relation between propositions (about a quantum mechanical system) and the projection onto the corresponding subspace of the space of quantum states is what is referred to as the “collapse of the wave function”.

- Kurt Engesser, Dov Gabbay, Daniel Lehmann,
*A New Approach to Quantum Logic*, vol. 8 of Studies in Logic, College Publications, London, UK, 2007. (pdf)

Last revised on May 13, 2021 at 20:09:35. See the history of this page for a list of all contributions to it.