Univalence and Constructive Identity

TL;DR

This paper explores how Homotopy Type Theory's non-standard identity concept offers a constructive and empirical perspective on identity judgments, exemplified by Frege's Venus case.

Contribution

It introduces a novel analysis of identity using Homotopy Type Theory, bridging empirical evidence and constructive reasoning.

Findings

Provides a new interpretation of Frege's Venus example

Shows how empirical evidence supports identity judgments in this framework

Highlights the constructive nature of identity in Homotopy Type Theory

Abstract

The non-standard identity concept developed in the Homotopy Type theory allows for an alternative analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities and accounts for the constructive aspect of such judgements.