disjunctive logic

**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**

*Disjunctive logic* is the internal logic of lextensive categories.

Created on April 26, 2011 14:45:19
by Urs Schreiber
(131.211.232.154)