Proof Theory of Constructive Systems: Inductive Types and Univalence

TL;DR

This paper explores the proof-theoretic foundations of constructive systems, examining inductive types, univalence, and their connections to various constructive frameworks like Martin-Lof type theory and explicit mathematics.

Contribution

It analyzes the proof-theoretic strength of constructive theories with inductive types and univalence, linking them to ordinal analysis and foundational frameworks.

Findings

Connections between explicit mathematics and type theories clarified

Strength of univalence axiom assessed through proof-theoretic methods

Ordinal-theoretic characterizations of constructive theories provided

Abstract

In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set theory. Proof theory has contributed to a deeper grasp of the relationship between different frameworks for constructive mathematics. Some of the reductions are known only through ordinal-theoretic characterizations. The paper also addresses the strength of Voevodsky's univalence axiom. A further goal is to investigate the strength of intuitionistic theories of generalized inductive definitions in the framework of intuitionistic explicit mathematics that lie beyond the reach of Martin-Lof type theory.