nLab induction - contents

• inductive type
• higher inductive type
• coinductive type

Rules

• induction, coinduction
• recursion, corecursion

Categorical semantics

• initial algebra of an endofunctor, terminal coalgebra of an endofunctor

• initial algebra of a presentable ∞-monad

Examples

• natural numbers object, natural numbers type

• list

• identity type

• W-type

• circle type

• interval type