اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدDoctrines, modalities and comonads
177
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Doctrines are categorical structures very apt to study logics of different nature within a unified environment: the 2-category Dtn of doctrines. Modal interior operators are characterised as particular adjoints in the 2-category Dtn. We show that they can be constructed from comonads in Dtn as well as from adjunctions in it, and the two constructions compare. Finally we show the amount of information lost in the passage from a comonad, or from an adjunction, to the modal interior operator. The basis for the present work is provided by some seminal work of John Power.
قيم البحث
اقرأ أيضاً
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of fac
torization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a localization higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature $
Sigma$ for a generalized algebraic theory and the associated category of cwfs with a $Sigma$-structure and cwf-morphisms that preserve this structure on the nose. Our definition refers to uniform families of contexts, types, and terms, a purely semantic notion. Furthermore, we show how to syntactically construct initial cwfs with $Sigma$-structures. This result can be viewed as a generalization of Birkhoffs completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjers construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families.
We introduce a notion of globular multicategory with homomorphism types. These structures arise when organizing collections of higher category-like objects such as type theories with identity types. We show how these globular multicategories can be u
sed to construct various weak higher categorical structures of types and terms.
Lovasz (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite structure C. Soon after, Pultr (1973) pro
ved a categorical generalisation of this fact. We propose a new categorical formulation, which applies to any locally finite category with pushouts and a proper factorisation system. As special cases of this general theorem, we obtain two variants of Lovasz theorem: the result by Dvov{r}ak (2010) that characterises equivalence of graphs in the k-dimensional Weisfeiler-Leman equivalence by homomorphism counts from graphs of tree-width at most k, and the result of Grohe (2020) characterising equivalence with respect to first-order logic with counting and quantifier depth k in terms of homomorphism counts from graphs of tree-depth at most k. The connection of our categorical formulation with these results is obtained by means of the game comonads of Abramsky et al. We also present a novel application to homomorphism counts in modal logic.
We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a more intricate judgemental structure than previous modal extensions of
Homotopy Type Theory. We use this theory to develop an synthetic approach to spectra, where spectra are represented by certain types, and constructions on them by type structure: maps of spectra by ordinary functions, loop spaces by the identity type, and so on. We augment the type theory with a pair of axioms, one which implies that the spectra are stable, and the other which relates synthetic spectra to the ordinary definition of spectra in type theory as $Omega$-spectra. Finally, we show that the type theory is sound and complete for an abstract categorical semantics, in terms of a category-with-families with a weak endomorphism whose functor on contexts is a bireflection, i.e. has a counit an a unit that are a section-retraction pair.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
