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

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

Profile

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

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 1920212223
24252627282930

Syndicate

RSS Atom

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 20th, 2017 02:09 am
Powered by Dreamwidth Studios