initial algebra of an endofunctor, terminal coalgebra of an endofunctor

initial algebra of a presentable ∞-monad

natural numbers object, natural numbers type

list

identity type

W-type

circle type

interval type

deductive reasoning, deduction

sequent

hypothesis/context/antecedent $\vdash$ conclusion/consequence/succedent

logical framework

deductive system,

natural deduction

sequent calculus

inductive reasoning

induction, recursion

inductive type, higher inductive type

induction over arbitrary well-ordered sets.

Created on July 4, 2017 at 07:56:56. See the history of this page for a list of all contributions to it.