Log in

Теория категорий [entries|friends|calendar]
Теория категорий

[ userinfo | livejournal userinfo ]
[ calendar | livejournal calendar ]


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.

post comment

Duality Theory and Categorical Universal Logic: With Emphasis on Quantum Structures [01 Apr 2016|04:55am]

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.

2 comments|post comment

Техническое [28 Mar 2016|09:10pm]

В это сообщество больше не пишу, поскольку оба модератора мудаки. Остаток учебника скоро выложу у себя в журнале и ещё здесь
9 comments|post comment

A van Kampen theorem for toposes [21 Feb 2016|01:52pm]
Упорядочивал библиотеку и наткнулся, наверное, на любопытное.

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.
post comment

Sylow theorems for ∞-groups [16 Feb 2016|06:15am]
Натолкнулся на забавное —
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.
3 comments|post comment

Homotopy Type Theory: A synthetic approach to higher equalities [20 Jan 2016|03:00pm]
Не знаю точно, сюда ли это, но наверное, в чём-то поможет понять, вот и...
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.
35 comments|post comment

Dependent Inductive and Coinductive Types are Fibrational Dialgebras [20 Jan 2016|11:28am]
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.
4 comments|post comment

Lawvere theories and Jf-relative monads [13 Jan 2016|01:17pm]
[by oskar_808]
Lawvere theories and Jf-relative monads
Vladimir Voevodsky
In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor
J f : F → Sets
where F is the category with the set of objects N and morphisms being the functions between the standard finite sets of the corresponding cardinalities.
The methods of this paper are fully constructive and it should be formalizable in the Zermelo-Fraenkel theory without the axiom of choice and the excluded middle.
It is also easily formalizable in the UniMath.
5 comments|post comment

«Спонтанное нарушение дуальности» [08 Jan 2016|02:56pm]

Дорогие товарищи и товарки! Заметил одну загадочную вещь.
Вот у нас есть терминальный объект — и есть инициальный. Есть уравнители — и коуравнители. Произведение и копроизведение. Ну и вообще принцип двойственности.
Всё хорошо, красиво, симметрично. Т.е. кажется, что привычка искать двойственные конструкции — это знание теории категорий на двоечку (на троечку, по утверждению nivanych — сопряжённые функторы и умение и везде увидеть). И, если полезна конструкция, то двойственная, вроде бы, тоже всегда полезна.
Наконец, мы приходим к экспонентам и... молчок. Слепое пятно. Заговор молчания.
Т.е., казалось бы, за 60 лет существования теории категорий можно было бы понять, что из себя представляют гипотетические "коэкспоненты" и зачем они нужны.
Ну ладно, допустим, у них нет применений в разработанных на сей момент теориях. Но тогда хотя бы один из авторов учебников должен озвучить: должны быть ещё коэкспоненты, но...
«А нэту». В чём дело? «Переписывание глупостей из учебника в учебник» (в данном случае — виде умолчаний)? Двойственность — более тонкое явление и нам выдают упрощённую версию? Или что?
(то же и с топосами, кстати, про «котопосы», кажется, никто из популярных авторов не упоминает — а казалось бы, это как раз должен быть нетривиальный результат, который трудно получить в рамках не-теоркатного подхода)
20 comments|post comment

A Compositional Framework for Passive Linear Networks [02 Jan 2016|06:08pm]
John C. Baez, Brendan Fong
Passive linear networks are used in a wide variety of engineering applications, but the best studied are electrical circuits made of resistors, inductors and capacitors.
We describe a category where a morphism is a circuit of this sort with marked input and output terminals.
In this category, composition describes the process of attaching the outputs of one circuit to the
inputs of another.
We construct a functor, dubbed the 'black box functor', that takes a circuit, forgets its internal structure, and remembers only its external behavior.
Two circuits have the same external behavior if and only if they impose same relation between currents and potentials at their terminals.
The space of these currents and potentials naturally has the structure of a symplectic vector space, and the relation imposed by a circuit is a Lagrangian linear relation.
Thus, the black box functor goes from our category of circuits to the category of symplectic vector spaces and Lagrangian linear relations.
We prove that this functor is a symmetric monoidal dagger functor between dagger compact categories.
We assume the reader has some familiarity with category theory, but none with circuit theory or symplectic linear algebra.
1 comment|post comment

A New Foundation for Representation in Cognitive and Brain Science: Category Theory and the Hippocam [29 Dec 2015|03:25pm]
Наверное, это всё же оффтопик...
Но прошу вас, не ругайтесь сильно ;-)

The thesis establishes correspondences between mathematical structures and brain structures.
The virtue of such a correspondence is that it makes available the powerful tools of the latter for the deduction of hypotheses for structure and function in neuropsychology.
Such an approach is relatively free from the vagaries of purely verbal reasoning and can offer novel insights into the intrinsic nature of cognitive phenomena.

It is unreasonable to think that purely linear mathematics can be the killer tool to model the complex interactions that take place in the brain.
We may indeed, need a new mathematical language for describing brain activity.

It sets the agenda of category theory as the appropriate methodology that provides the necessary theoretical framework in order to understand the structure of complex systems, like the brain, in mathematical terms.
Although category theory at first sight may seem too pure and universal, in contrast with the spurious biological realm, where the particular prevails over the universal;
it may lead to a new and deeper insight into the structure and the representational power of the brain.
The thesis paves the way for a more synthetic methodology in cognitive science, the scale free dynamics hypothesis is studied with a new “categorical” light.

In addition, it provides a theory of hippocampus structure and function based on category theory.
In particular, it demonstrates that the co-operation of the grid fields may give rise to a “colimit” which is a place field.


[by zeit_raffer]
3 comments|post comment

Globular, a new proof assistant for working with higher-categorical proofs using string diagrams. [07 Dec 2015|11:54am]
The purpose of this post is to introduce Globular, a new proof assistant for working with higher-categorical proofs using string diagrams.
It’s available at
with documentation on the nlab.
It’s web-based, so everything happens right in your browser:
build formal proofs, visualize and step through them;
keep your proofs private, share them with collaborators, or make them publicly available.

3 comments|post comment

Ещё одно введение в категории [06 Dec 2015|01:46pm]
[by zeit_raffer]
Якобы для программистов (скорее, для компутерных ученых), но материал очень продвинутый.

Pierre-Louis Curien
Category theory: a programming language-oriented introduction

Нет оглавления, что неудобно, но пролистал.
Довольно много рассказывают про моноидальные диаграммы,
которыми он дальше пользуется для более наглядного изложения темы про (ко)алгебры.
Расширения Кана излагаются идеологически грамотно.
Вроде, всё хорошо и правильно — предварительно, одобряю ;-)
1 comment|post comment

Забывающие из категории моноидальных категорий [04 Nov 2015|04:20pm]
Рассмотрим забывающие функторы из, например, категории симметричных замкнутых и просто моноидальных категорий в Cat.
Как должны выглядеть левые сопряжённые к ним?
В случае симметричных замкнутых, получаем просто свободное присоединение декартового произведения и экспоненты?
А в случае просто моноидальных, неужели просто декартовое произведение?
Что-то не то.
Ну и далее, рассуждения про получившуюся монаду и алгебры для неё.
Что это за логики получаются такие универсальные?

Скорее всего, ответ тут должен быть какой-то простой, но что-то я буксую...
16 comments|post comment

Категорная семантика сетей Петри [18 Oct 2015|11:37am]
Максим тут подкинул статью —
A Taste of Categorial Petri Nets
Claudia Ermel, Alfio Martini
В ней относительно внятно рассказывается про категорию сетей Петри, про копределы в ней (суть — склейка сетей для построения сложного из простого).
Он пытается использовать эти идеи для верификации эрланга —
Наверное, я плохо понял статью — не получилось состряпать самостоятельно ни экспоненты ни классификатор.Collapse )
9 comments|post comment

начать теорию категорий с полиграфов [13 Oct 2015|03:31pm]
получилось зарегистрироваться...
а то что-то с картигками глючило..

сейчас я могу сам завести тему такую - начать теорию категорий с полиграфов -
ваши книги и книгу Георгия туда можно включить тогда... (или наоборот),
делаем попытку построения теории категорий сразу с поликатегорий, начать просто, а как говорят Козловский и Гарнер - мы должны столкнуться с огромными трудностями ... ну давайте дойдем до этих трудностей, зато ясность и естественность строить категории со стрелок имеющих несколько выходов и входов изначально имеется, кстати у программистов такие стрелки наверняка до всяких категорий должны встречатьтся, есть ли ссылки на подобные статьи?
13 comments|post comment

Еще одно введение в категории [15 Sep 2015|12:15pm]
An invitation to General Algebra and Universal Constructions
by George M. Bergman
(расчитано на математиков)
Узнал от
57 comments|post comment

Категория уравнений в частных производных над гладким многообразием образует топос! [07 Jun 2015|04:38pm]
Вот —
Узнал от

Не знаю прям, что мне теперь делать с этим знанием? %)
Мозговправляюще весьма.
33 comments|post comment

Category Theory in Coq 8.5 [26 May 2015|06:44pm]
Category Theory in Coq 8.5
Amin Timany, Bart Jacobs
We report on our experience implementing category theory in Coq 8.5.
The repository of this development can be found at
This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.
post comment

Хаскельное — Categories of Structures in Haskell [26 May 2015|12:28pm]
Сомневался, сюда ли это статья...
Но решил, что таки сюда —
Наслаждайтесь ;-)
post comment

[ viewing | most recent entries ]
[ go | earlier ]