Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Matteo Spadetto

TL;DR

The paper addresses the problem of conservativity between extensional and propositional dependent type theories by leveraging homotopy-theoretic concepts. It develops a semantic framework based on categories with attributes and canonical homotopy equivalences to identify contexts and types up to homotopy, then constructs a quotient model that interprets an Extensional Type Theory exactly over a Propositional Theory restricted to h-sets. The main contributions are the introduction of canonical context/type equivalences, the construction of a semantic context category and its display maps, and the demonstration that Extensional Type Theory is conservative over Propositional Type Theory (augmented with UIP for the concluding step) for judgments about h-sets. This yields a semantic route to conservativity results in dependent type theories with propositional computation rules, linking extensional reasoning to a range of propositional judgments and offering a robust foundation for interpreting propositional type theories within an extensional framework. The results have implications for understanding equality, identity types, and computation rules in type-theoretic foundations and may inform formalizations in proof assistants and univalent foundations.

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.

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

TL;DR

The paper addresses the problem of conservativity between extensional and propositional dependent type theories by leveraging homotopy-theoretic concepts. It develops a semantic framework based on categories with attributes and canonical homotopy equivalences to identify contexts and types up to homotopy, then constructs a quotient model that interprets an Extensional Type Theory exactly over a Propositional Theory restricted to h-sets. The main contributions are the introduction of canonical context/type equivalences, the construction of a semantic context category and its display maps, and the demonstration that Extensional Type Theory is conservative over Propositional Type Theory (augmented with UIP for the concluding step) for judgments about h-sets. This yields a semantic route to conservativity results in dependent type theories with propositional computation rules, linking extensional reasoning to a range of propositional judgments and offering a robust foundation for interpreting propositional type theories within an extensional framework. The results have implications for understanding equality, identity types, and computation rules in type-theoretic foundations and may inform formalizations in proof assistants and univalent foundations.

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.
Paper Structure (32 sections, 39 theorems, 157 equations, 9 figures)

This paper contains 32 sections, 39 theorems, 157 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Preliminary conventions and terminology
  3. Recap on categories with attributes
  4. Extending substitution to terms
  5. Variable terms
  6. Semantics of extensional and propositional type theories
  7. Homotopy equivalences of contexts in Propositional Type Theory
  8. Extension of context homotopy equivalences
  9. Dependent product of homotopy equivalences
  10. Dependent sum of homotopy equivalences
  11. Identity types over homotopy equivalent types
  12. Canonical homotopy equivalences between types
  13. Canonical homotopy equivalences between contexts
  14. Properties of the canonical homotopy equivalences
  15. Properties of the family of canonical equivalences
  16. ...and 17 more sections

Key Result

Proposition 2.3

Let $(\mathcal{C},\textsc{tp},-.-,P)$ be a category with attributes. Let $f$ be a semantic context morphism $\Gamma \to \Delta.B$, where $B$ is a semantic type in $\Delta$. Then there is a unique semantic term $\overline{f}$ of $B[P_Bf]$ in $\Gamma$ such that the diagram: \begin{tikzcd} \Gamma \arro for some semantic context morphism $\Gamma \xrightarrow{g}\Delta$ and some semantic term $b$ of $B[

Figures (9)

  • Figure 1: Extensional identity types
  • Figure 2: Intensional identity types
  • Figure 3: Propositional identity types
  • Figure 4: Dependent product types
  • Figure 5: Propositional dependent product types
  • ...and 4 more figures

Theorems & Definitions (68)

  • Definition 2.1: Category with attributes
  • Remark 2.2: Notation and terminology
  • Proposition 2.3
  • Proposition 2.4
  • Proposition 2.5
  • Lemma 2.6
  • Remark 2.7
  • Lemma 2.8
  • Lemma 2.9
  • Remark 2.10
  • ...and 58 more