Skip to main content
Proof Assistants Beta

About

Ask Question
Tag Info
Info Newest Frequent Score Active Unanswered

In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)

References:
nLab
Wikipedia
Lean
Coq

History Excerpt history