64 citations · 78 across the 9 of their papers we have counts for
6 papers · 1 filter
Makkai's lost proof of projectivity of N in the free topos
Henrik Forssell, Peter LeFanu Lumsdaine, Andrew W. Swan
We give a categorical proof of the projectivity of in the free topos -- in proof-theoretic terms, the rule of countable choice for intuitionistic higher-order logic -- based on…
Constructive completeness and non-discrete languages
Henrik Forssell, Christian Espíndola
We give an analysis and generalizations of some long-established constructive completeness results in terms of categorical logic and pre-sheaf and sheaf semantics. The purpose is i…
Constructive reflectivity principles for regular theories
Henrik Forssell, Peter LeFanu Lumsdaine
Classically, any structure for a signature may be completed to a model of a desired regular theory by means of the chase construction or small object argument. Moreover, th…
Type theoretical databases
Henrik Forssell, Håkon Robbestad Gylterud, David I. Spivak
We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of intere…
Topological Representation of Geometric Theories
Henrik Forssell
Using Butz and Moerdijk's topological groupoid representation of a topos with enough points, a `syntax-semantics' duality for geometric theories is constructed. The emphasis is on…
First-Order Logical Duality
Steve Awodey, Henrik Forssell
From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as pres…