Relating homotopy equivalences to conservativity in dependent type theories with computation axioms

TL;DR

This paper establishes a conservativity result for extensional type theories over propositional ones by leveraging homotopy type theory concepts, showing their equivalence for reasoning about h-sets.

Contribution

It introduces a novel approach using homotopy equivalences and categories with attributes to relate extensional and propositional dependent type theories.

Findings

Extensional and propositional type theories are equivalent for h-set judgments.

Homotopy equivalences provide a semantic bridge between different type theories.

The approach simplifies reasoning about dependent types with computation axioms.

Abstract

We prove a conservativity result for extensional type theories over propositional ones, i.e. dependent type theories with propositional computation rules, or computation axioms, using insights from homotopy type theory. The argument exploits a notion of canonical homotopy equivalence between contexts, and uses the notion of a category with attributes to phrase the semantics of theories of dependent types. Informally, our main result asserts that, for judgements essentially concerning h-sets, reasoning with extensional or propositional type theories is equivalent.