Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

When is the partial map classifier a Sierpiński cone?

Leoni Pugh, Jonathan Sterling

Abstract

We study the relationship between partial map classifiers, Sierpiński cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic $\infty$-categories are closed under partial map classifiers assuming Phoa's principle, and we isolate a new reflective subuniverse of types within which the Sierpiński cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition.

When is the partial map classifier a Sierpiński cone?

Abstract

We study the relationship between partial map classifiers, Sierpiński cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic -categories are closed under partial map classifiers assuming Phoa's principle, and we isolate a new reflective subuniverse of types within which the Sierpiński cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition.

Paper Structure

This paper contains 1 section, 25 theorems, 15 equations, 2 tables.

Table of Contents

  1. Omitted proofs

Key Result

Lemma 2

Any totally ordered interval is a bounded distributive lattice satisfying the disjunction principle.

Theorems & Definitions (43)

  • Definition 1
  • Lemma 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Remark 7
  • Definition 8
  • Lemma 9: Structure identity principle for Sierpiński data
  • Lemma 10: Comparison map
  • ...and 33 more