Constructor subtyping in the Calculus of Inductive Constructions
The Calculus of Inductive Constructions (CIC) is a powerful type
system, featuring dependent types and inductive definitions, that
forms the basis of proof-assistant systems such as Coq and Lego.
We extend CIC with constructor subtyping, a basic form of subtyping
in which an inductive type A is viewed as a subtype of another
inductive type B if B has more elements than A.
It is shown that the calculus is well-behaved and provides a suitable
basis for formalizing natural semantics in proof-development systems.