arXiv subjects

Sam Speight

Publications and source records attributed to Sam Speight.

4 recordsLinked to original sources

arXiv2026

Impredicativity in Linear Dependent Type Theory

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

cs.LO↗

arXiv2025

A Structural Account of Combinatory Completeness

We give a general notion of combinatory completeness with respect to a faithful cartesian club and use it systematically to obtain characterisations of a number of different kinds of applicative system. Moreover, we characterise combinatory completeness of a given applicative system in terms of multicategory structure on its computable maps.

math.CT↗

arXiv2024

Groupoidal Realizability for Intensional Type Theory

We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit of realizability, this is intended to formalize a homotopical BHK interpretation, whereby evidence for an identification is a path. Specifically, we study partitioned groupoidal assemblies. Categories of such are parameterised by "realizer categories" (instead of the usual partial combinatory algebras) that come equipped with an interval qua internal cogroupoid. The interval furnishes a notion of homotopy as well as a fundamental groupoid construction. Objects in a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category; isomorphisms in the base groupoid are realized by paths in said fundamental groupoid. The main result is that, under mild conditions on the realizer category, the ensuing category of partitioned groupoidal assemblies models intensional (1-truncated) type theory without function extensionality. Moreover, when the underlying realizer category is "untyped", there exists an impredicative universe of 1-types (the modest fibrations). This is a groupoidal analogue of the traditional situation.

cs.LO↗

arXiv2018

Impredicative Encodings of (Higher) Inductive Types

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

cs.LO↗