antecedent

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

A judgement on the left of the “$\vdash$”-symbol of a sequent/hypothetical judgement.

A *hypothesis* or *context*.

**antecedents** $\vdash$ succedents

**antecedents** $\vdash$ consequent

Last revised on September 26, 2012 at 14:12:53. See the history of this page for a list of all contributions to it.