Вопрос про 2-категории

Начал кодировать (инфинити,1)-категории и сразу же столкнулся с проблемой кодировкаи Hom функтора 3-категории. Кроме категории естественный преобрзований, где морфизмы — это так называемые модификации (следующий уровень после естественных преобразований), надо в 3-категории включить информацию о предыдущих категориях, для предыдущей 2-категории — это объекты двух видов: 1) категории в категории категории; 2) функторы в категории функторов.

Я посмотрел на правила вертикальной и горизонтальной композиции, которые включены уже в категорию категорий и категорию функторов, и мне кажется, что существует изоморфизм между, с одной стороны — декартовым произведением двух категорий: категорией категорий и категорией функторов, и с другой стороны — 2-категорией. Вопрос, так ли это, и если да, то существует ли где-то такая теорема?

Продублировал вопрос тут: https://dxdy.ru/topic127434.html (с более сильной теоремой про бикатегории, которые в сущности более слабые версии 2-категорий).

Emily Riehl - Category Theory in Context

Table of contents
Chapter 1. Categories, Functors, Natural Transformations
Chapter 2. Universal Properties, Representability, and the Yoneda Lemma
Chapter 3. Limits and Colimits
Chapter 4. Adjunctions
Chapter 5. Monads and their Algebras
Chapter 6. All Concepts are Kan Extensions
Epilogue: Theorems in Category Theory

(внутри ссылка на бесплатный pdf)


We will elsewhere comment on the relation of our relative monads to the recent gen- eralization of monads by Spivey [31] that was also motivated by programming examples: he fixes a functor K ∈ C → J (notice the direction) to then look for monad-like structures with an underlying functor J → C. With Paul Levy we have checked that a fair amount of monad theory transfers to his generalized monads, but they are not monoids in [J, C] unless K has a left adjoint, in which case they are equivalent to relative monads. Sam Staton has considered an enriched variant of relative monads.


Duality Theory and Categorical Universal Logic: With Emphasis on Quantum Structures

Yoshihiro Maruyam

Categorical Universal Logic is a theory of monad-relativised hyperdoctrines (or fibred universal al- gebras), which in particular encompasses categorical forms of both first-order and higher-order quan- tum logics as well as classical, intuitionistic, and diverse substructural logics. Here we show there are those dual adjunctions that have inherent hyperdoctrine structures in their predicate functor parts. We systematically investigate into the categorical logics of dual adjunctions by utilising Johnstone- Dimov-Tholen’s duality-theoretic framework. Our set-theoretical duality-based hyperdoctrines for quantum logic have both universal and existential quantifiers (and higher-order structures), giving rise to a universe of Takeuti-Ozawa’s quantum sets via the tripos-to-topos construction by Hyland- Johnstone-Pitts. The set-theoretical hyperdoctrinal models of quantum logic, as well as all quantum hyperdoctrines with cartesian base categories, turn out to give sound and complete semantics for Faggian-Sambin’s first-order quantum sequent calculus over cartesian type theory; in addition, quan- tum hyperdoctrines with monoidal base categories are sound and complete for the calculus over linear type theory. We finally consider how to reconcile Birkhoff-von Neumann’s quantum logic and Abramsky-Coecke’s categorical quantum mechanics (which is modernised quantum logic as an antithesis to the traditional one) via categorical universal logic.


A van Kampen theorem for toposes

Упорядочивал библиотеку и наткнулся, наверное, на любопытное.

A van Kampen theorem for toposes
Marta Bunge and Stephen Lack

In this paper we introduce the notion of an extensive 2-category, to be thought of as "2-category of generalized spaces".
We consider and extensive 2-category K equipped with a binary-product-preserving pseudofunctor C : K_op → Cat, which we think of as specifying the "coverings" of the generalized spaces.
We prove, in this context, a van Kampen theorem which generalizes and refines one of Brown and Janelidze.
The local properties required in this theorem are stated in terms of morphism of effective descent for the pseudofunctor C.
We specialize the general van Kampen theorem to the 2-category Top_S of toposes bounded over an elementary topos S, and to its full sub-2-category LTop_S determined by the locally connected toposes, after showing both of these 2-categories to be extensive.
We then consider three particular notions of coverings on toposes corresponding respectively to local homeomorphisms, covering projections, and unramified morphisms;
in each case we deduce a suitable version of a van Kampen theorem in terms of coverings and, under further hypotheses, also one in terms of fundamental groupoids.
An application is also given to knot groupoids and branched coverings.
Along the way we are led to investigate locally constant objects in a topos bounded over an arbitrary base topos S and to establish some new facts about them.

Sylow theorems for ∞-groups

Натолкнулся на забавное —
Sylow theorems for ∞-groups
Matan Prasma, Tomer M. Schlank
(Submitted on 14 Feb 2016)
Viewing Kan complexes as ∞-groupoids implies that pointed and connected Kan complexes are to be viewed as ∞-groups.
A fundamental question is then: to what extent can one "do group theory" with these objects?
In this paper we develop a notion of a finite ∞-group:
an ∞-group with finitely many non-trivial homotopy groups which are all finite.
We prove a homotopical analog of the Sylow theorems for finite ∞-groups.
We derive two corollaries:
the first is a homotopical analog of the Burnside's fixed point lemma for p-groups
and the second is a "group-theoretic" characterization of (finite) nilpotent spaces.

Homotopy Type Theory: A synthetic approach to higher equalities

Не знаю точно, сюда ли это, но наверное, в чём-то поможет понять, вот и...
Homotopy Type Theory: A synthetic approach to higher equalities
Michael Shulman
This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher."
Ask an average mathematician or philosopher today about the foundations of mathematics, and you are likely
to receive an answer involving set theory: an apparent consensus in marked contrast to the foundational
debates of the early 20th century.
Now, at the turn of the 21st century, a new theory has emerged to challenge the foundational ascendancy of sets.
Arising from a surprising synthesis of constructive intensional type theory and abstract homotopy theory, Homotopy Type Theory and Univalent Foundations (hott/uf) purports to represent more faithfully the everyday practice of mathematics, but also provides powerful new tools and a new paradigm.
So far, its concrete influence has been small, but its potential implications for mathematics and philosophy are profound.

Dependent Inductive and Coinductive Types are Fibrational Dialgebras

Dependent Inductive and Coinductive Types are Fibrational Dialgebras
Henning Basold
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types.
It is well-known that dependent type theories à la Martin-Löf can be interpreted using fibrations.
Modern theorem provers, however, are based on more sophisticated type systems that allow the definition of powerful inductive dependent types (known as inductive families) and, somewhat limited, coinductive dependent types.
I define a class of functors on fibrations and show how data type definitions correspond to initial and final dialgebras for these functors.
This description is also a proposal of how coinductive types should be treated in type theories, as they appear here simply as dual of inductive types.
Finally, I show how dependent data types correspond to algebras and coalgebras, and give the correspondence to dependent polynomial functors.