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
basic constructions:
strong axioms
further
The notion of coinductive types is dual to that of inductive types.
Where the categorical semantics of an inductive type is an initial algebra for an endofunctor, the semantics of a coinductive type is a terminal coalgebra of an endofunctor.