arXiv subjects
Publications and source records attributed to Andrew W. Swan.
We give a categorical proof of the projectivity of $N$ in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on the unpublished proof of Michael Makkai (c.1980). The presentation aims to be self-contained and accessible to any reader acquainted with elementary toposes and their logic.
We give a categorical formulation of Kraus' "magic trick" for recovering information from truncated types. Rather than type theory, we work in Van den Berg-Moerdijk path categories with a univalent universe, and rather than propositional truncation we work with arbitrary cofibrations, which includes truncation as a special case. We show, using Kraus' argument that any cofibration with homogeneous domain is a monomorphism. We give some simple concrete examples in groupoids to illustrate the interaction between homogeneous types, cofibrations and univalent fibrations.
We give a construction of classifiers for double negation stable h-propositions in a variety of cubical set models of homotopy type theory and cubical type theory. This is used to give some relative consistency results: classifiers for double negation stable propositions exist in cubical sets whenever they exist in the metatheory; the Dedekind real numbers can be added to homotopy type theory without changing the consistency strength; we construct a model of homotopy type theory with extended Church's thesis, which states that all partial functions with double negation stable domain are computable.
Definability is a key notion in the theory of Grothendieck fibrations that characterises when an external property of objects can be accessed from within the internal logic of the base of a fibration. In this paper we consider a generalisation of definability from properties of objects to structures on objects, introduced by Shulman under the name local representability. We first develop some general theory and show how to recover existing notions due to B\'{e}nabou and Johnstone as special cases. We give several examples of definable and non definable notions o structure, focusing on algebraic weak factorisation systems, which can be naturally viewed as notions of structure on codomain fibrations. Regarding definability, we give a sufficient criterion for cofibrantly generated awfs's to be definable, generalising a construction of the universe for cubical sets, but also including some very different looking examples that do not satisfy tininess in the internal sense, that exponential functors have a right adjoint. Our examples of non definability include the identification of logical principles holding for the interval objects in simplicial sets and Bezem-Coquand-Huber cubical sets that suffice to show a certain definition of Kan fibration is not definable.