The Internal Logic and Finite Colimits
William Troiani
TL;DR
This work develops an internal-language framework for describing finite colimits inside a topos that admits countably infinite colimits, translating classical set-theoretic constructions into the Mitchell-Benabou language. It analyzes the key distinction between internal (intensional) unions and external (extensional) unions, providing internal constructions for initial objects, finite coproducts, and coequalisers, and then assembling these to obtain finite colimits in general topoi. The approach is demonstrated in the topos of Sets and extended to arbitrary topoi, supported by a system of derived rules to ensure soundness of the internal logic. Overall, the paper offers a rigorous method to reason about and construct finite colimits within topos-theoretic contexts using the internal logic, strengthening formalization capabilities in categorical logic.
Abstract
We describe how finite colimits can be described using the internal lanuage, also known as the Mitchell-Benabou language, of a topos, provided the topos admits countably infinite colimits. This description is based on the set theoretic definitions of colimits and coequalisers, however the translation is not direct due to the differences between set theory and the internal language, these differences are described as internal versus external. Solutions to the hurdles which thus arise are given.