64 citations · 78 across the 9 of their papers we have counts for
10 papers
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…
On Equivalence and Cores for Incomplete Databases in Open and Closed Worlds
Henrik Forssell, Evgeny Kharlamov, Evgenij Thorstensen
Data exchange heavily relies on the notion of incomplete database instances. Several semantics for such instances have been proposed and include open (OWA), closed (CWA), and open-…
Generating Ontologies from Templates: A Rule-Based Approach for Capturing Regularity
Henrik Forssell, Christian Kindermann, Daniel P. Lupp +2
We present a second-order language that can be used to succinctly specify ontologies in a consistent and transparent manner. This language is based on ontology templates (OTTR), a…
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…
Filtered Colimit Preserving Functors on Models of a Regular Theory
Henrik Forssell
This note recalls the representation of regular theories T in terms of set-valued functors on models given by Makkai(1990), and explicitly states the representation theorem for the…
Subgroupoids and Quotient Theories
Henrik Forssell
Moerdijk's site description for equivariant sheaf toposes on open topological groupoids is used to give a proof for the (known, but apparently unpublished) proposition that if H is…
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…