bamalip: (NGE)
другой вывод, более конструктивный, который можно обнаружить, рассмотрев нашу конструкцию в контексте n-категорий: кодирование инициальных объектов пределами можно не только обобщить на высшие размерности, но и упростить в размерности нуль, при этом получится исходная кодировка Черча. Это то, чего долго хотелось - единой стройной картины без мистики, объясняющей, почему стирание (erasure) предела дает нам Черча. Оказывается, стирание - это декатегорификация, при которой мы от (1,1)-категорий и конструкций на них переходим к (0,1)-категориям и конструциям на них. 2-морфизмы (равенства сетоидов) при этом испаряются. От обычного предела на сетоидах после такой операции остается обычное теор-типовое зависимое произведение, которое мы и видим в Черче-Берардуччи. Ура!

Другая сторона медали - повышение размерности - состоит в том, что мы можем строить всякие 2-пределы или 2-копределы на 1-категориях при помощи несложного (в непредикативном случае несложного...) обобщения кодировки. Это дает возможность, в том числе, вычислять всякие "индуктивно определенные категории", вроде категории последовательностей объектов на исходной категории. Эта часть нашего механизма работает.

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:47 pm
Powered by Dreamwidth Studios