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, list,

• identity type

• W-type

Edit this sidebar