Interactive proof assistants represent inductive data and induction principals differently depending on the underlying type theory. The most well-known proof assistant, Coq, utilizes a complicated implementation of an intrinsic calculus of inductive constructions. Cedille is a proof assistant based on a pure extrinsic type theory with a notably small core implementation in which induction principles are generically derivable for data and computation represented as lambda encoded F-algebras.
This is a sandbox for my masters thesis project.