Godels Dialectica interpretation was designed to obtain a relative consistency proof for Heyting arithmetic, to be used in conjunction with the double negation interpretation to obtain the consistency of Peano arithmetic. In recent years, proof theor
etic transformations (so-called proof interpretations) that are based on Godels Dialectica interpretation have been used systematically to extract new content from proofs and so the interpretation has found relevant applications in several areas of mathematics and computer science. Following our previous work on Godel fibrations, we present a (hyper)doctrine characterisation of the Dialectica which corresponds exactly to the logical description of the interpretation. To show that we derive in the category theory the soundness of the interpretation of the implication connective, as expounded on by Spector and Troelstra. This requires extra logical principles, going beyond intuitionistic logic, Markovs Principle (MP) and the Independence of Premise (IP) principle, as well as some choice. We show how these principles are satisfied in the categorical setting, establishing a tight (internal language) correspondence between the logical system and the categorical framework. This tight correspondence should come handy not only when discussing the applications of the Dialectica already known, like its use to extract computational content from (some) classical theorems (proof mining), its use to help to model specific abstract machines, etc. but also to help devise new applications.
A well-known theorem of Buchweitz provides equivalences between three categories: the stable category of Gorenstein projective modules over a Gorenstein algebra, the homotopy category of acyclic complexes of projectives, and the singularity category.
To adapt this result to $N$-complexes, one must find an appropriate candidate for the $N$-analogue of the stable category. We identify this $N$-stable category via the monomorphism category and prove Buchweitzs theorem for $N$-complexes over a Frobenius exact abelian category. We also compute the Serre functor on the $N$-stable category over a self-injective algebra and study the resultant fractional Calabi-Yau properties.
We provide axioms that guarantee a category is equivalent to that of continuous linear functions between Hilbert spaces. The axioms are purely categorical and do not presuppose any analytical structure. This addresses a question about the mathematica
l foundations of quantum theory raised in reconstruction programmes such as those of von Neumann, Mackey, Jauch, Piron, Abramsky, and Coecke.
Under a general categorical procedure for the extension of dual equivalences as presented in this papers predecessor, a new algebraically defined category is established that is dually equivalent to the category $bf LKHaus$ of locally compact Hausdor
ff spaces and continuous maps, with the dual equivalence extending a Stone-type duality for the category of extremally disconnected locally compact Hausdorff spaces and continuous maps. The new category is then shown to be isomorphic to the category $bf CLCA$ of complete local contact algebras and suitable morphisms. Thereby, a new proof is presented for the equivalence ${bf LKHaus}simeq{bf CLCA}^{rm op}$ that was obtained by the first author more than a decade ago. Unlike the morphisms of $bf CLCA$, the morphisms of the new category and their composition law are very natural and easy to handle.
In this paper, we generally describe a method of taking an abstract six functors formalism in the sense of Khan or Cisinski-D{e}glise, and outputting a derived motivic measure in the sense of Campbell-Wolfson-Zakharevich. In particular, we use this f
ramework to define a lifting of the Gillet-Soue motivic measure.
In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map $f$ is independent of the ZFC ax
ioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable (possibly large) family of maps, a reflective subuniverse of any universe $mathcal{U}$. When specialized to an appropriate family, this produces a localization which when interpreted in the $infty$-topos of spaces agrees with the localization corresponding to $E$. Our approach generalizes the approach of [CSS] in two ways. First, by working in homotopy type theory, our construction can be interpreted in any $infty$-topos. Second, while the local objects produced by [CSS] are always 1-types, our construction can produce $n$-types, for any $n$. This is new, even in the $infty$-topos of spaces. In addition, by making use of universes, our proof is very direct. Along the way, we prove many results about small types that are of independent interest. As an application, we give a new proof that separated localizations exist. We also give results that say when a localization with respect to a family of maps can be presented as localization with respect to a single map, and show that the simplicial model satisfies a strong form of the axiom of choice which implies that sets cover and that the law of excluded middle holds.
It is shown that the category of emph{semi-biproducts} of monoids is equivalent to the category of emph{pseudo-actions}. A semi-biproduct of monoids is a new notion, obtained through generalizing a biproduct of commutative monoids. By dropping commut
ativity and requiring some of the homomorphisms in the biproduct diagram to be merely identity-preserving maps, we obtain a semi-biproduct. A pseudo-action is a new notion as well. It consists of three ingredients: a pre-action, a factor system and a correction system. In the category of groups all correction systems are trivial. This is perhaps the reason why this notion, to the authors best knowledge, has never been considered before.
We recall several categories of graphs which are useful for describing homotopy-cohere
We introduce the category of finite strings and study its basic properties. The category is closely related to the augmented simplex category, and it models categories of linear representations. Each lattice of non-crossing partitions arises naturally as a lattice of subobjects.
Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are kn
own to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categories as particular cases, and are adapted to mechanized computations. We show that a finite rewriting system in precategories admits a finite number of critical pairs, which can be efficiently computed. We also extend Squiers theorem to our context, showing that a convergent rewriting system is coherent, which means that any two parallel 3-cells are necessarily equal. This allows us to prove coherence results for several well-known structures in the context of Gray categories: monoids, adjunctions, Frobenius monoids.
