On the internal structures of inductive types

摘要

the paper investigates the internal structures of hereditaryinductive types in logical types theory. By defining a bisimulationequality on the inhabitants of each hereditary inductive type, one isable to show that the inhabitants of a hereditary inductive typesatisfy the basic properties of sets. A hereditary inductive type cantherefore be conceived as a universe of sets.