Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Toward the effective 2-topos

Steve Awodey, Jacopo Emmenegger

TL;DR

This work proposes a concrete path to a realizability-inspired $(2,1)$-topos $\mathcal{E}\!f\!f_2$ whose $0$-types recover the effective topos $\mathcal{E}\!f\!f$, addressing limitations of naive higher-topos constructions in constructive settings. It analyzes $\mathcal{E}\!f\!f$ as the 1-exact completion of the partitioned-assemblies category $\mathcal{P}$ and introduces coherent presheaves $\mathsf{Coh}$, showing $\mathsf{Coh}$ realizes $\mathcal{E}\!f\!f$; then it builds a presheaf-of-groupoids framework and defines coherent groupoids via pseudo-compact diagonals. The main result proves that every coherent fibrant $0$-type $\mathbb{G}$ is equivalent to a discrete coherent object, yielding $\mathsf{Coh}\mathsf{Gpd}(\widehat{\mathcal{P}})_0 \simeq \mathsf{Coh}(\widehat{\mathcal{P}}) \simeq \mathcal{E}\!f\!f$, thereby realizing a candidate $(2,1)$-realizability topos for higher-type foundations. This establishes a pathway toward univalence and higher-type interpretations of realizability in a robust, internal-logical setting with potential practical impact for foundations of higher-type computation and logic.

Abstract

A candidate for the effective 2-topos is proposed and shown to include the effective 1-topos as its subcategory of 0-types.

Toward the effective 2-topos

TL;DR

This work proposes a concrete path to a realizability-inspired -topos whose -types recover the effective topos , addressing limitations of naive higher-topos constructions in constructive settings. It analyzes as the 1-exact completion of the partitioned-assemblies category and introduces coherent presheaves , showing realizes ; then it builds a presheaf-of-groupoids framework and defines coherent groupoids via pseudo-compact diagonals. The main result proves that every coherent fibrant -type is equivalent to a discrete coherent object, yielding , thereby realizing a candidate -realizability topos for higher-type foundations. This establishes a pathway toward univalence and higher-type interpretations of realizability in a robust, internal-logical setting with potential practical impact for foundations of higher-type computation and logic.

Abstract

A candidate for the effective 2-topos is proposed and shown to include the effective 1-topos as its subcategory of 0-types.

Paper Structure

This paper contains 5 sections, 18 theorems, 11 equations.

Table of Contents

  1. Introduction
  2. The effective 1-topos
  3. Coherent groupoids
  4. The main result
  5. Related and Future work

Key Result

Proposition 1

For a regular category $\mathcal{R}$, the exact completion (preserving regular epis) can be described as the full subcategory of sheaves for the regular topology, on those objects $E$ with an exact presentation by representables: thus those for which there is a kernel-quotient diagram in which $R, R'\in \mathcal{R}$ and $\mathsf{y}{R'} \rightrightarrows \mathsf{y}{R}$ is the kernel pair of $\mat

Theorems & Definitions (33)

  • Proposition 1: Lack1999
  • Proposition 2
  • proof
  • Lemma 3
  • proof
  • Lemma 4
  • proof
  • Lemma 5
  • proof
  • Definition 6
  • ...and 23 more