Вопрос про Бикатегории

[5HT]

Начал кодировать (инфинити,1)-категории и сразу же столкнулся с проблемой кодировкаи Hom функтора 3-категории. Кроме категории естественный преобрзований, где морфизмы — это так называемые модификации (следующий уровень после естественных преобразований), надо в 3-категории включить информацию о предыдущих категориях, для предыдущей 2-категории — это объекты двух видов: 1) категории в категории категории; 2) функторы в категории функторов.

Я посмотрел на правила вертикальной и горизонтальной композиции, которые включены уже в категорию категорий и категорию функторов, и мне кажется, что существует изоморфизм между, с одной стороны — декартовым произведением двух категорий: категорией категорий и категорией функторов, и с другой стороны — бикатегорией. Вопрос, так ли это, и если да, то существует ли где-то такая теорема?

[george66]

Не знаю, но почти наверняка нет. В этой теории ничего просто не бывает.

[5HT]

Вот я решил закодировать первые 7 элементов 2-категории: 0,1,2-клетки, 1-id, 2-id, 1-compose, 2-compose.
С вашего позволения буду использовать кубический синтаксис https://github.com/mortberg/cubicaltt:

Базовое определение Категории и Функтора:

cat: U = (A: U) * (A -> A -> U)
isPrecategory (C: cat): U
  = (id: (x: C.1) -> C.2 x x)
  * (c: (x y z:C.1) -> C.2 x y -> C.2 y z -> C.2 x z)
  * (homSet: (x y: C.1) -> isSet (C.2 x y))
  * (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f)
  * (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f)
  * ((x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) ->
    Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
precategory: U = (C: cat) * isPrecategory C

catfunctor (A B: precategory): U
  = (ob: carrier A -> carrier B)
  * (mor: (x y: carrier A) -> hom A x y -> hom B (ob x) (ob y))
  * (id: (x: carrier A) -> Path (hom B (ob x) (ob x)) (mor x x (path A x)) (path B (ob x)))
  * ((x y z: carrier A) -> (f: hom A x y) -> (g: hom A y z) ->
     Path (hom B (ob x) (ob z)) (mor x z (compose A x y z f g))
      (compose B (ob x) (ob y) (ob z) (mor x y f) (mor y z g)))

Определение категории категорий и категории функторов:

Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = precategory
    Hom (A B: Ob): U = catfunctor A B
    id (A: Ob): catfunctor A A = idFunctor A
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = compFunctor A B C f g
    ...

Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = catfunctor X Y
    Hom (A B: Ob): U = ntrans X Y A B
    id (A: Ob): ntrans X Y A A = ...
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = ...
    ...

Определение 2-категорий (первых 7 элементов):

Cat2 : U
     = (Ob: U)
     * (Hom: (A B: Ob) -> U)
     * (Hom2: (A B: Ob) -> (C F: Hom A B) -> U)
     * (id: (A: Ob) -> Hom A A)
     * (id2: (A: Ob) -> (B: Hom A A) -> Hom2 A A B B)
     * (c:  (A B C: Ob) (f: Hom A B) (g: Hom B C) -> Hom A C)
     * (c2: (A B: Ob) (X Y Z: Hom A B)
            (f: Hom2 A B X Y) (g: Hom2 A B Y Z) -> Hom2 A B X Z)
     * ...

Доказательство, что 2-категория изоморфна (или может быть представлена через, или существует encode/decode с ректрактом и секцией) декартовому произведению категории категорий и категории функторов:

Cat2Impl1 : Cat2
        = ( {- Ob -}   Cat.1.1,
            {- Hom -}  \ (X Y: Cat.1.1) -> (Func X Y).1.1,
            {- Hom2 -} \ (X Y: Cat.1.1) -> (Func X Y).1.2,
            {- id -}   Cat.2.1,
            {- id2 -}  \ (A: Cat.1.1)   -> (Func A A).2.1,
            {- c -}    Cat.2.2.1,
            {- c2 -}   \ (X Y: Cat.1.1) -> (Func X Y).2.2.1,
            ... )

Тот же трюк (построение экземпляра 2-категории как декартовое умножение некоторых катагорий) можно проделать с еще двумя категориями — категорией множеств и категорией функций (с точностью до альфа конверсии тоже самое):

Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = SET
    Hom (A B: Ob): U = A.1 -> B.1
    id (A: Ob): Hom A A = idfun A.1
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = o A.1 B.1 C.1 g f
    HomSet (A B: Ob): isSet (Hom A B) = setFun A.1 B.1 B.2
    ...

Functions (X Y: U) (Z: isSet Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
     Ob: U = X -> Y
     Hom (A B: Ob): U = id (X -> Y)
     id (A: Ob): Hom A A = idfun (X -> Y)
     c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = idfun (X -> Y)
     HomSet (A B: Ob): isSet (Hom A B) = setFun Ob Ob (setFun X Y Z)
     ...

Набросок доказательства тут: https://github.com/groupoid/infinity/bl ... tegory.ctt

-- 01.06.2018, 17:43 --

Выше мы работаем в пре-стрикт 2-категории. Напомню, что Бикатегория — это слабая 2-категория, ее определение вот такое (урезанное, но тоже кишащее произведениями):

Bicategory : U
     = (Ob: U)
     * (Hom: (A B: Ob)  -> precategory)
     * (id: (A: Ob)     -> catfunctor unitCat  (Hom A A))
     * (c:  (A B C: Ob) -> catfunctor (Product (Hom B C) (Hom A B)) (Hom A C))
     * (c2: (A B C: Ob) (L R: precategory)
                        -> catfunctor L (Hom B C)
                        -> catfunctor R (Hom A B)
                        -> catfunctor (Product L R) (Hom A C)) * unit

Ваш Максим