The text treats fundamental design differences between set theoretic and type theoretic foundations, led by the more or less justified deployment of sameness in the case of isomorphic mathematical structures, specifically groups. We refresh the necessary knowledge of set theory and progress via an in-depth presentation of Martin-Löf's type theory, acknowledging elementary concepts regarding types and the rules they obey, the constructive logic implemented by the propositions as types correspondence and present the peculiar identity types, resulting in the general notion of equality. We construct the type of groups. The univalence axiom is introduced following a rather technical construction of the univalence type, enabling us to sketch a proof of the structure identity principle for the special case of groups. Remarks are given when different approaches in both foundational theories emerge. The h-level classification of types is subsequently provided together with two special subclasses from it, behaving as sets and propositions.
|
