nLab
computational trinitarianism

Idea

Under the identifications

1. propositions as types

2. programs as proofs

3. relation between type theory and category theory

the following notions are equivalent:

1. A proof of a proposition. (In logic.)

2. A program with output some type. (In type theory and computer science.)

3. A generalized element of an object. (In category theory.)

This is referred to as “computational trinitarianism” in (Harper), where also an exposition is given.

The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

Computational trinitarianism entails that any concept arising in one aspect should have meaning from the perspective of the other two. If you arrive at an insight that has importance for logic, languages, and categories, then you may feel sure that you have elucidated an essential concept of computation–you have made an enduring scientific discovery. (Harper)

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

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-level 1-type/h-prop
proof	generalized element	program
conjunction	product	product type
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 monad	modal type theory, monad (in computer science)

References

A concise exposition of the relation between the three concepts is

• Robert Harper, The Holy Trinity (2011) (web)

An exposition that also suggests some connections to physics is in

• John Baez, Mike Stay, Physics, Topology, Logic and Computation: A Rosetta Stone, Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174 (arXiv:0903.0340)

For further references see at programs as proofs, propositions as types, and relation between category theory and type theory.