я краем уха слышал, что половина всего, что касается бикатегории Cat можно обобщить на какие-то другие бикатегории
в случае, если ты хочешь обобщить 2-морфизмы, получается тебе нужна какая-то 3-категория.
Но я чисто на удачу сболтнул, @Comonoid вот лучше ответит

> если ты хочешь обобщить 2-морфизмы,
> получается тебе нужна какая-то 3-категория
Таких вещей много и "повышение уровня" неким "правильным образом", позволяет делать, в том числе, и интернализацию.
О чём именно имеется в виду, я пока не догадался.
С первого взгляда, просто 2-категории вполне обобщают Cat ;-)
Если что-то рядом с предпучками, то сразу однозначно надо вспомнить структуры Йонеды.
"обобщить 2-морфизмы" тоже можно разными способами.
Стоило бы ещё Пашу спросить, может быть, он бы лучше понял вопрос... Но...

>  просто 2-категории вполне обобщают Cat
ну если оставить просто 2-категорию, тогда совокупность 2-ячеек для пары заданных 1-ячеек останется множеством
как я понимаю, автор хочет, чтобы там вместо множеств были объекты какой-то категории

Моя мысль такая - результаты зависящие от категории множеств возможно усилить ослабив категорию множеств.

до какой-нибудь категории попроще

Ну если так, то это называется "обогащение", и тогда, это будет напрямую 3-категорией.
Это одна из двух распостранённых конструкций построения строгих n-категорий — последовательное обогащение.

Тогда надо внимательно смотреть, какие конструкции используются и в каких более общих категориях у них есть аналоги.

ну хомотопический Set и есть уже некоторое обобщение
в данном случае Set - это клас всех классов, равенства на которых пруф-иррелевантны

мы не требуем всяких роскошей типа LEM

Нуу, боюсь, что это не совсем элементарная категория будет.
Кажется, всё-таки придётся иметь внутри неё кванторы.

Иначе, как-то про параметричность придётся рассуждать ad hoc.

Дане, лишнее это всё.
Если я правильно понимаю, то сама категория может быть простой, типа декартово-замкнутой с копроизведениями и well-pointed.
И в основном, надо будет уметь доказывать строго все эти изоморфизмы типаа
(a+b)→c  ~  (a→c) * (b→c)

О, я теперь знаю как переводится энричмент на русский!

А что значит "усилить результаты"?

ослабить условия

охладите свои условия

A => B, A => A1 и A1 =/> A, вдруг A1 => B тоже верно

Ну часть результатов теорката можно перенести на интернал категорию в любом топосе, например

Часть результатов можно перенести на любую обогощённую категорию

Но ослабляя условия меньше теорем доказывается. По-моему это очевидно :)