Related papers: Open Horn Type Theory
This is the final version of a series of papers uploaded in May 25, 2005. We have splitted the long last paper of the previous version in two parts to make it easier to understand. The results are essentially the same, although the…
In this note, we prove an obstruction theorem for the existence of A infinite-structures over a commutative ring R on an algebra A associative up to homotopy, in terms of the Hochschild cohomology of the associative algebra H(A). The hidden…
We describe a category, the objects of which may be viewed as models for homotopy theories. We show that for such models, ``functors between two homotopy theories form a homotopy theory'', or more precisely that the category of such models…
Attractor-repeller decompositions of isolated invariant sets give rise to so-called connecting homomorphisms. These homomorphisms reveal information on the existence and structure of connecting trajectories of the underlying dynamical…
We establish a categorical framework relating two canonical model constructions in first-order logic: the Henkin construction and compactness-based constructions via ultraproducts or saturation. By introducing a globally fixed set of Henkin…
In quantum logical terms, Hardy-type arguments can be uniformly presented and extended as collections of intertwined contexts and their observables. If interpreted classically those structures serve as graph-theoretic "gadgets" that enforce…
Naturally occurring diagrams in algebraic topology are commutative up to homotopy, but not on the nose. It was quickly realized that very little can be done with this information. Homotopy coherent category theory arose out of a desire to…
When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties…
Compositionality is at the heart of computer science and several other areas of applied category theory such as computational linguistics, categorical quantum mechanics, interpretable AI, dynamical systems, compositional game theory, and…
This is the fourth in a series of papers extending Martin-L\"of's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of…
We develop an obstruction theory for the extension of truncated minimal $A$-infinity bimodule structures over truncated minimal $A$-infinity algebras. Obstructions live in far-away pages of a (truncated) fringed spectral sequence of…
We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the…
A characteristic property of cohomology with compact support is the long exact sequence that connects the compactly supported cohomology groups of a space, an open subspace and its complement. Given an arbitrary cohomology theory of…
Statements analogous to the Hard Lefschetz Theorem (HLT) and the Hodge-Riemann bilinear relations (HRR) hold in a variety of contexts: they impose restrictions on the cohomology algebra of a smooth compact K\"ahler manifold or on the…
The Holant theorem is a powerful tool for studying the computational complexity of counting problems in the Holant framework. Due to the great expressiveness of the Holant framework, a converse to the Holant theorem would itself be a very…
Escard\'o and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher-inductive notion of reals, and suggests that the interval may satisfy…
We examine the class of languages that can be defined entirely in terms of provability in an extension of the sorted type theory (Ty_n) by embedding the logic of phonologies, without introduction of special types for syntactic entities.…
In this paper we define a rigid rational homotopy type, associated to any variety $X$ over a perfect field $k$ of positive characteristic. We prove comparison theorems with previous definitions in the smooth and proper, and log-smooth and…
DEKL 2.0 is a dependent type-theoretic framework for trace-indexed knowledge evolution. Its central claim is that the proof calculus remains monotone under standard structural rules, while non-monotonic behavior arises semantically from…
An Independent Parallelism Theorem is proven in the theory of adhesive HLR categories. It shows the bijective correspondence between sequential independent and parallel independent direct derivations in the Weak Double-Pushout framework,…