Log in

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

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

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

This is the (co)end, my only (co)friend [07 May 2015|10:46am]
"Раз пошла такая пьянка" и у ivan_gandhi
в его блоге постоянно стали упоминаться
(ко)концы и расширения Кана, то возник повод
вспомнить и про соответствующую статью ;-)
Кое-кто будет на неё ругаться и даже обзываться,
но я таки отрекламирую —

This is the (co)end, my only (co)friend
Fosco Loregian
The present note is a recollection of the most striking and useful applications of co/end calculus.
We put a considerable effort in making arguments and constructions rather explicit:
after having given a series of preliminary definitions, we characterize co/ends as particular co/limits;
then we derive a number of results directly from this characterization.
The last sections discuss the most interesting examples where co/end calculus serves as a powerful abstract way to do explicit computations in diverse fields like Algebra, Algebraic Topology and Category Theory.
The appendices serve to sketch a number of results in theories heavily relying on co/end calculus;
the reader who dares to arrive at this point, being completely introduced to the mysteries of co/end fu, can regard basically every statement as a guided exercise.
4 comments|post comment

A first-order logic for string diagrams [05 May 2015|10:42am]
Ещё всем известные тов. Joyal & Street немало постарались формализовать "Tensor Calculus".
Вот некая попытка сделать шаг вперёд —
A first-order logic for string diagrams
Aleks Kissinger, David Quick
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category.
This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation.
While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes.
In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic called with conjunction, implication, and universal quantification over !-boxes.
This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes.
We then build a standard model for !L and give an example proof of a theorem яfor non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
1 comment|post comment

[12 Apr 2015|09:50pm]

Человек говорит, что в параграфе про декартовы квадраты все линии без стрелок. Я смотрю Adobe Reader и стрелки вижу. Есть такая проблема или нет?

P.S. Проблемы нет "В Evince на Debian — не видны при масштабе 125% и менее"
5 comments|post comment

Учебник, версия 8 [29 Mar 2015|05:37am]



Уравнители, декартовы квадраты, топосы, монады, чуть-чуть про Мартин-Лёфа. Главу про монады, в принципе, можно читать сразу, хотя я поместил её в конец. Но не обещаю, что будет просто, хотя я старался. Совсем простая наука, видимо, закончилась. Напишу ещё одну серию (про пределы) и составлю, наконец, указатель, с которым были трудности из-за палёного миктеха. Буду рад критике.

P.S. "Можно читать сразу" тем, кто читал седьмую версию, конечно.
65 comments|post comment

[20 Dec 2014|11:34pm]

И теперь вопрос, что мне дальше писать. Чисто категорного материала осталось мало (пределы и копределы). Я хотел ещё написать большую развесистую главу про лямбда-исчисление, но тут выбор такой:
1) Писать, как Барендрегт (то есть, замалчивать самые сложные места);
2) Писать лучше Барендрегта, но для этого в данный момент у меня нет авторитета, отложим до лучших времён.
Замечено две опечатки и один умеренный ляп в не самом важном месте. Так что склоняюсь к тому, чтобы дописать пределы и копределы, исправить опечатки и пока закончить. Могу также разбить главу про сопряжённость на несколько разделов поменьше.
Вообще, первоначально был план "написать популярную брошюрку страниц на сто", план уже перевыполнен в два раза, пора заканчивать.
4 comments|post comment

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