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

TL;DR

This paper introduces a new way to represent the language of a topos using quotients of span categories, and explores their logical relations and categorical properties.

Contribution

It develops a novel framework for representing topos languages via span category quotients and analyzes their logical and categorical structures.

Findings

Boolean toposes form a reflective subcategory of toposes

Quotients of span categories effectively model topos languages

Logical functors preserve the structure between toposes

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.