20 citations · 82 across the 18 of their papers we have counts for
20 papers
On the -topos semantics of homotopy type theory
Emily Riehl
Many introductions to homotopy type theory and the univalence axiom gloss over the semantics of this new formal system in traditional set-based foundations. This expository article…
Double negation stable h-propositions in cubical sets
Andrew W. Swan
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…
Definable and Non-definable Notions of Structure
Andrew W. Swan
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…
On the Nielsen-Schreier Theorem in Homotopy Type Theory
Andrew W Swan
We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated…
A class of higher inductive types in Zermelo-Fraenkel set theory
Andrew Swan
We define a class of higher inductive types that can be constructed in the category of sets under the assumptions of Zermelo-Fraenkel set theory without the axiom of choice or the…
Random spanning forests and hyperbolic symmetry
Roland Bauerschmidt, Nicholas Crawford, Tyler Helmuth +1
We study (unrooted) random forests on a graph where the probability of a forest is multiplicatively weighted by a parameter per edge. This is called the arboreal gas model, a…
Analyticity for rapidly determined properties of Poisson Galton--Watson trees
Yuval Peres, Andrew Swan
Let be a Galton--Watson tree with Poisson() offspring, and let be a tree property. In this paper, are concerned with the regularity of the function $\mathbb{P}_λ(A):=…
On Church's Thesis in Cubical Assemblies
Andrew Swan, Taichi Uemura
We show that Church's thesis, the axiom stating that all functions on the naturals are computable, does not hold in the cubical assemblies model of cubical type theory. We show tha…
The geometry of random walk isomorphism theorems
Roland Bauerschmidt, Tyler Helmuth, Andrew Swan
The classical random walk isomorphism theorems relate the local times of a continuous-time random walk to the square of a Gaussian free field. A Gaussian free field is a spin syste…
Identity Types in Algebraic Model Structures and Cubical Sets
Andrew Swan
We give a general technique for constructing a functorial choice of very good paths objects, which can be used to implement identity types in models of type theories in direct mann…
Separating Path and Identity Types in Presheaf Models of Univalent Type Theory
Andrew Swan
We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves. The main result is that path type…
Lifschitz Realizability as a Topological Construction
Michael Rathjen, Andrew Swan
We develop a number of variants of Lifschitz realizability for CZF by building topological models internally in certain realizability models. We use this to show some interesting m…
On Dividing by Two in Constructive Mathematics
Andrew Swan
A classic result due to Bernstein states that in set theory with classical logic, but without the axiom of choice, for all sets and , if then a…
Every metric space is separable in function realizability
Andrej Bauer, Andrew Swan
We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with syntheti…
W-Types with Reductions and the Small Object Argument
Andrew Swan
We define a simple kind of higher inductive type generalising dependent -types, which we refer to as -types with reductions. Just as dependent -types can be characterised…
Lifting Problems in Grothendieck Fibrations
Andrew Swan
Many interesting classes of maps from homotopical algebra can be characterised as those maps with the right lifting property against certain sets of maps (such classes are sometime…
Dynkin isomorphism and Mermin--Wagner theorems for hyperbolic sigma models and recurrence of the two-dimensional vertex-reinforced jump process
Roland Bauerschmidt, Tyler Helmuth, Andrew Swan
We prove the vertex-reinforced jump process (VRJP) is recurrent in two dimensions for any translation invariant finite range initial rates. Our proof has two main ingredients. The…
Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory
Andrew Swan
The existence of least finite support is used throughout the subject of nominal sets. In this paper we give some Brouwerian counterexamples showing that constructively, least finit…
An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof
Andrew Swan
We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of…
CZF does not have the Existence Property
Andrew W Swan
Constructive theories usually have interesting metamathematical properties where explicit witnesses can be extracted from proofs of existential sentences. For relational theories,…