arXiv subjects

Andrew Swan

Publications and source records attributed to Andrew Swan.

46 records · Page 3Linked to original sources

arXiv2019

Most white dwarfs with detectable dust discs show infrared variability

Archival data from the WISE satellite reveals infrared flux variations of tens of per cent around numerous dusty white dwarfs. Data spanning more than seven years reveal more than half of known systems are varying in the 3.4 micron band, while the 4.6 micron data are challenging to interpret due to lower signal-to-noise. The sparsely-sampled data limit interpretation, but the heterogeneous light curves suggest each source may be idiosyncratic, where there maybe competing processes operating on different time-scales. Collisions are likely driving the observed decays in flux, and this finding suggests that dust production is operating more often than indicated by previous observations. The observed variation is at odds with the canonical flat disc model in isolation, and underscores the need for infrared monitoring of these evolved planetary systems to inform the next generation of theoretical models.

astro-ph.SR↗

arXiv2018

Separating Path and Identity Types in Presheaf Models of Univalent Type Theory

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 types cannot be used directly as identity types in any Orton-Pitts style model of univalent type theory with propositional truncation in presheaf assemblies over the first and second Kleene algebras. We also give a Brouwerian counterexample showing that there is no constructive proof that there is an Orton-Pitts model of type theory in presheaves when the universe is based on a standard construction due to Hofmann and Streicher, and path types are identity types. A similar proof shows that path types are not identity types in internal presheaves in realizability toposes as long as a certain universe can be extended to a univalent one. We show that one of our key lemmas has a purely syntactic variant in intensional type theory and use it to make some minor but curious observations on the behaviour of cofibrations in syntactic categories.

math.LO↗

arXiv2018

Identity Types in Algebraic Model Structures and Cubical Sets

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 manner with little reliance on general coherence results. We give a simple proof that applies in algebraic model structures that possess a notion of structured weak equivalence, in a sense that we define here. We then give a more direct proof that applies both to the original BCH cubical set model and more recent variants. We give an explanation how this construction relates to the one used in the CCHM cubical set model of type theory.

math.CT↗

arXiv2018

Lifschitz Realizability as a Topological Construction

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 metamathematical results about constructive set theory with variants of LLPO including consistency with unique Church's thesis, consistency with some Brouwerian principles and variants of the numerical existence property.

math.LO↗

arXiv2018

On Dividing by Two in Constructive Mathematics

A classic result due to Bernstein states that in set theory with classical logic, but without the axiom of choice, for all sets $X$ and $Y$, if $X \times 2 \cong Y \times 2$ then also $X \cong Y$. We show that this cannot be done in constructive mathematics by giving some examples of toposes where it fails.

math.LO↗

arXiv2018

W-Types with Reductions and the Small Object Argument

We define a simple kind of higher inductive type generalising dependent $W$-types, which we refer to as $W$-types with reductions. Just as dependent $W$-types can be characterised as initial algebras of certain endofunctors (referred to as polynomial endofunctors), we will define our generalisation as initial algebras of certain pointed endofunctors, which we will refer to as pointed polynomial endofunctors. We will show that $W$-types with reductions exist in all $ΠW$-pretoposes that satisfy a weak choice axiom, known as weakly initial set of covers (WISC). This includes all Grothendieck toposes and realizability toposes as long as WISC holds in the background universe. We will show that a large class of $W$-types with reductions in internal presheaf categories can be constructed without using WISC. We will show that $W$-types with reductions suffice to construct some interesting examples of algebraic weak factorisation systems (awfs's). Specifically, we will see how to construct awfs's that are cofibrantly generated with respect to a codomain fibration, as defined in a previous paper by the author.

math.CT↗

arXiv2018

Lifting Problems in Grothendieck Fibrations

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 sometimes referred to as cofibrantly generated). In a more sophisticated notion due to Garner (referred to as algebraically cofibrantly generated) the set of maps is replaced with a diagram over a small category. We give a yet more general definition where the set or diagram of maps is replaced with a vertical map in a Grothendieck fibration. In addition to an interesting new view of the existing examples above, we get new notions, such as computable lifting problems in presheaf assemblies, and internal lifting problems in a topos. We show that under reasonable conditions one can define a notion of universal lifting problem and carry out step-one of Garner's small object argument. We give explicit descriptions of what the general construction looks like in some examples.

math.CT↗

arXiv2017

Evidence of the Poisson/Gaudin-Mehta phase transition for banded matrices on global scales

We prove that the Poisson/Gaudin--Mehta phase transition conjectured to occur when the bandwidth of an $N \times N$ symmetric banded matrix grows like $\sqrt N$ is observable as a critical point in the fourth moment of the level density for a wide class of symmetric banded matrices. A second critical point when the bandwidth grows like ${2 \over 5} N$ leads to a new conjectured phase transition in the eigenvalue localization, whose existence we demonstrate in numerical experiments.

math.PR↗

arXiv2017

Some Brouwerian Counterexamples Regarding Nominal Sets in Constructive Set Theory

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 finite support does not always exist and in fact can be quite badly behaved. On this basis we reinforce the point that when working constructively with nominal sets the use of least finite support should be avoided. Moreover our examples suggest that this problem can't be fixed by requiring nominal sets to have least finite support by definition or by using the notion of subfinite instead of finite.

math.LO↗

arXiv2016

An Algebraic Weak Factorisation System on 01-Substitution Sets: A Constructive Proof

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 Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorization systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J computation rule is absent from the original cubical set model and suggest a way to fix this.

math.LO↗