Категорная модель higher order типов -- это топос.
Категорная модель зависимых типов -- это Local CCC.

Естественно, что все-все возможные системы
с зависимыми типами на практике не нужны.
Какие-то из них вполне впихиваются в топосы.

Так вот, меня взяло сомнение, а все ли "полезные"
системы типов могут упихаться в некоторый топос?...
Есть ли какая очень нужная и полезная система
с зависимыми типами, которая не описывается топосом
(топосом из топосов и функторов между ними)?...

( Дополнение )

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

( ТУТ )

Только двигаюсь очень медленно.

Многие видели пример в Coq -
Constructive Category Theory
(она сделана на setoid'ах).

Помнится, у меня были, в общем-то,
примитивные мысли про построение
чего-то подобного на основе OTT.

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

В ходе ленивого гугления на эти темы
обнаружил вот такие (менее примитивные)
мысли на тему OTT и Predicative Topos -
http://www.nabble.com/Re:-Definitional-equality-in-observational-type-theory-p8717336.html

И в частности -
I do indeed think that
Observational Type Theory with quotient types
should be the language of a Predicative Topos.

Разберусь во всём этом, буду себя страшно уважать ;-)
Вот.

Introduction to Higher Order Categorical Logic
By J. Lambek, P. J. Scott
http://books.google.com/books?hl=en&id=6PY_emBeGjUC&dq=Introduction+to+Categorical+Logic&printsec=frontcover&source=web&ots=AtgZH6r_kd&sig=r7600AFWh-r-qghA94qPdMsz78U&sa=X&oi=book_result&resnum=4&ct=result

Очень интересная книжка !

( Классики, крута ! )

Ещё одну книжку нашёл -
B. Jacobs, Categorical Logic and Type Theory
Вот содержание ->
http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html

На гугле только "демонстрашка",
чтобы понять, что книжка интересная.

Обе книжки есть у меня в электронном виде.
Обе более 30 мег.

Ну, с чего-то, хоть и небольшого, я уже начал.

Описание, что такое морфизмы, объекты, категории (худо-бедно, сделал).

Потом более подробное объяснение языка диаграмм.
В дальнейших объяснениях всё больше и больше
его использовать, до уровня, который сочту нужным.
[Как только я буду столько рисовать-то в тексте ??
Может, попытаться на SVG, например ?]

Эпи-моно-изо-морфизмы, их примеры в нескольких категориях.
В качестве примера, наверное, рассказать про
категорное определение подобъекта и отличие
этого определения от теоретико-множественного.
Возможно, стоит кратко рассказать про классификатор подобъектов.

Начальные-терминальные объекты, показать их дуальность.
Теперь можно объяснить про декартовое произведение,
копроизведение, и наверное, про экспоненту с её свойствами ...

Дальше, наверное, можно рассказывать про функторы,
что они бывают (ко-контр)вариантные.
Пример категории функторов, примеры разных функторов,
вот тут надо побольше привести.

Не уверен, нужно ли рассказывать про
естественное преобразование и лемму Йонеды ...
Наверное, надо. Если по McLane'у, то это вообще основы ;-)

Потом нужна большая куча примеров.

Приблизительно вот так ...