3 citations · 3 across the 1 of their papers we have counts for
4 papers · 1 filter
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…
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…
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…
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…