Конструктивная теория категорий не очень конструктивна? И типа того. Непричёсанные мысли.
Все (из тех, что я видел) теории категорий,
которые назывались конструктивными, лично я
такими бы не назвал, разве только формально,
раз уж изложили их внутри конструктивной логики.


Возьму всем знакомый и близкий по духу
пример предела -- произведение.
Повторю классическое определение.
Произведение a и b -- это объект,
обозначаемый (a,b), со стрелками-проекциями
pia : (a,b) -> a
pib : (a,b) -> b
и чтобы для любого объекта c с двумя стрелками
f : c -> a
g : c -> b
существовала, и притом одна стрелка ku : c -> (a,b)
чтобы диаграмма, из всех этих стрелок нарисованная,
была коммутативна, то есть, чтобы
pia o ku = f
pib o ku = g
(Зачем так расписывал? Ну раз уж написал, удалять не буду.)
Написать про пределы, что-ли... не буду, и так многа букаф.

Ну и в такой вот логике, если у нас есть произведение,
мы можем рассуждать, что для каждого c есть единственная ku,
и более того, в логике предикатов можем про правилу E
оперировать этим самым ku, как будто оно реально существует.

Теперь посмотрим "конструктивное" определение.
Там (a,b) задаётся вместе со способом построения
дял любого c единственной стрелки ku.
Да, спобоб построения и всё такое -- конструктивно.
Но как, имея объекты a и b, построить их произведение,
если даже ты точно знаешь, что оно существует?...

Иначе говоря, для близких сердцу категорий, в которых
существуют близкие сердцу пределы (или же вообще все конечные)
придётся строить совсем другую конструктивную теорию категорий.
Только такая теория будет полезна для народного хозяйства,
так как в той "конструктивной" непонятно, как построить даже простейшие
(ко)пределы типа (ко)произведений или даже терминального объекта.

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

Напомню, что при этих условиях категория уже становится
конечно-полной (finitely complete) и более того, даже
конечно-кополной (finitely cocomplete), а (по определению)
это значит, что в ней существуют любые конечные (ко)пределы,
и в частности, такие замечательные вещи, как
equalizer'ы и pullback'и (кстати, как по-русски?).

Нужен ли классификатор подобъектов?

Конечно-полные-кополные категории с экспонентами --
это уже довольно-таки много информации о категории.
Если говорить о конструкциях, то есть, о чём-то типа
языка программирования, то в зависимости от базы,
на которой стороится язык, как правило, легко доказывается,
существует ли там классификатор подобъектов или нет.

Иначе -- если категория уже зафиксирована, то классификатор
нельзя ввести дополнительно, так как если он не существует,
то получаем противоречивую теорию, а если существует,
то единственен с точностью до изоформизма.

Подустал я чего-то.
Не раскрыто много вопросов...
Как будут приходить в голову, буду писать.
А они будут приходить, обязательно.

Добавлю, посмотрите вот это --
Easy Categories for Programmers
http://docs.google.com/View?docid=dc7rg5cv_24ftbwjrgm