Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Representing the language of a topos as quotient of the category of spans

M. Golshani, A. Shiralinasab Langari

TL;DR

The paper addresses how to represent the internal language of a topos using quotients of span categories, and extends the treatment of indeterminate arrows to a simultaneous, universal framework. It constructs $Span_\Pi(\mathcal{C}, \Pi)$ to freely adjoin all indeterminates and shows that, when $\mathcal{C}$ is cartesian closed, $Span_\Pi(\mathcal{C}, \Pi)$ remains cartesian closed, enabling a coherent internal language interpretation. It then develops logical relations on span categories, proving that suitable quotients yield power allegories whose maps form a topos, and uses this to canonically Booleanize a topos, producing a reflective subcategory of $\mathsf{Top}$ called $\mathsf{BoolTop}$. The framework yields a universal, functorial construction of a Boolean topos associated to any elementary topos and clarifies how logical functors interact with these Booleanizations, with potential applications to internal reasoning and topos-theoretic semantics.

Abstract

We use quotients of span categories to introduce the language of a topos. We also study the logical relations and the quotients of span categories derived from them. As an application we show that the category of Boolean toposes is a reflective subcategory of the category of toposes, when the morphisms are logical functors.

Representing the language of a topos as quotient of the category of spans

TL;DR

The paper addresses how to represent the internal language of a topos using quotients of span categories, and extends the treatment of indeterminate arrows to a simultaneous, universal framework. It constructs to freely adjoin all indeterminates and shows that, when is cartesian closed, remains cartesian closed, enabling a coherent internal language interpretation. It then develops logical relations on span categories, proving that suitable quotients yield power allegories whose maps form a topos, and uses this to canonically Booleanize a topos, producing a reflective subcategory of called . The framework yields a universal, functorial construction of a Boolean topos associated to any elementary topos and clarifies how logical functors interact with these Booleanizations, with potential applications to internal reasoning and topos-theoretic semantics.

Abstract

We use quotients of span categories to introduce the language of a topos. We also study the logical relations and the quotients of span categories derived from them. As an application we show that the category of Boolean toposes is a reflective subcategory of the category of toposes, when the morphisms are logical functors.
Paper Structure (6 sections, 26 theorems, 40 equations)

This paper contains 6 sections, 26 theorems, 40 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Adding indeterminate arrows
  4. Language of a topos
  5. Logical relations on span categories
  6. Booleanization of a topos

Key Result

lemma 1

Let $\mathcal{F}$ be a stable system. Then $(s, f) \sim_{\mathcal{F}} (s', f')$ if and only if there exist $p, q \in \mathcal{F}$ such that the following diagram commutes: \xymatrix{ && D \ar[lld]_s \ar[rrd]^f && \\ A && P \ar[d]_q \ar[u]^p && B \\ && D' \ar[ull]^{s'} \ar[urr]_{f'} && }

Theorems & Definitions (35)

  • lemma 1: hsty
  • lemma 2
  • proposition 1
  • Theorem 1
  • proposition 2
  • Theorem 2
  • Theorem 3
  • corollary 1
  • Theorem 4
  • Theorem 5
  • ...and 25 more