Abstraction, equality and univalence

Area of Science:

• Foundations of mathematics
• Logic
• Computer science

Background:

• The Univalent Foundations Program (UFP) offers a novel approach to the foundations of mathematics.
• It integrates Martin-Löf type theory with a homotopic interpretation and Voevodsky's univalence axiom.
• This framework provides a new perspective on fundamental mathematical concepts.

Purpose of the Study:

• To provide a conceptual discussion of the Univalent Foundations Program.
• To analyze the relationship between propositional equality and indiscernibility within type theory.
• To investigate the validity of Leibniz's principle of the identity of indiscernibles in UFP.

Main Methods:

• Conceptual analysis of Martin-Löf type theory enriched with homotopic interpretation.
• Examination of the univalence axiom and its implications.
• Philosophical analysis of Leibniz's principle within the UFP framework.

Main Results:

• Propositional equality in type theory encodes the notion of indiscernibility.
• The homotopic interpretation of Martin-Löf type theory is addressed.
• Univalence is presented as a constructive abstraction resolving Fregean abstraction.

Conclusions:

• Univalent Foundations provides a framework where propositional equality aligns with indiscernibility.
• The univalence axiom offers a novel perspective on abstraction and identity.
• The study contributes to the understanding of identity and individuality in mathematics.