{- Category Theory: http://groupoid.space/mltt/types/category/
   - Examples: Set, Cat, Func, Ab.
   Copyright (c) Groupoid Infinity, 2014-2018. -}

module category where
import cat
import fun
import adj
import set
import proto
import algebra
import iso_sigma

-- The general notion of (∞,1)-categories

-- 0-cat   -- 0-ob are elements, 0-hom is equivalence relation, setoid -- sets
-- 1-cat   -- 1-ob are sets or 0-cat, 1-hom are maps
-- 2-cat-A -- 2-ob are 1-cat, 1-hom are functors/maps        \ bounded
-- 2-cat-B -- 2-ob are 1-cat, 2-hom are ntrans/mapsOnMaps    / definition
-- 3-cat-A -- 2-ob are (2-cat-A,2-cat-B), 1-hom are functors of product categories \
-- 3-cat-B -- 2-ob are (2-cat-A,2-cat-B), 2-hom are ntrans of product categories    ) morphisms
-- 3-cat-C -- 3-ob are (2-cat-A,2-cat-B), 3-hom are modifications                  /

-- Enrichment

--   (0-cat = Hom(A,B)         = A = B)
-- ↪ (1-cat = Hom(0-cat,0-cat) = set -> 0-cat)
-- ↪ (2-cat = Hom(1-cat,1-cat) = (set -> 0-cat) -> 1-cat)
-- ↪ (3-cat = Hom(2-cat,2-cat) = ((set -> 0-cat) -> 1-cat) -> 2-cat)

-- The general notion of k-morphisms

-- equiv        0-hom: U = undefined
-- functor      1-hom (C D: 1-cat): U = undefined
-- ntrans       2-hom (C D: 1-cat) (F G: 1-hom C D): U = undefined
-- modification 3-hom (C D: 1-cat) (F G: 1-hom C D) (I J: 2-hom C D F G): U = undefined

-- 1-Category of Sets
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
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
     : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
     = refl (Hom A D) (c A B D f (c B C D g h))

-- 2-Category with 1-hom morphisms (functors)
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
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined

-- AwodeyCT Definition 7.9. The functor category
-- 2-Category of Functors F: X -> Y with 2-hom morphisms (natural transformations)
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 = undefined
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = undefined
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined

-- Lemma. Monoid Hom is Set
setmonoidhom (a b: monoid)
  : isSet (monoidhom a b)
  = setSig (a.1.1 -> b.1.1) (ismonoidhom a b) setf setm where
    setf : isSet (a.1.1 -> b.1.1)
         = setPi a.1.1 (\ (_: a.1.1) -> b.1.1) (\ (_: a.1.1) -> b.1.2)
    setm (f: a.1.1 -> b.1.1)
         : isSet (ismonoidhom a b f)
         = propSet (ismonoidhom a b f) (propismonoidhom a b f)

-- Category of Commutative Monoids
CMon: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = cmonoid
    Hom (A B: Ob): U = cmonoidhom A B
    id (A: Ob): Hom A A = idmonoidhom (A.1,A.2.1)
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C
      = monoidhomcomp (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) f g
    HomSet (A B: Ob): isSet (Hom A B) = setmonoidhom (A.1, A.2.1) (B.1, B.2.1)
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f
      = lemma_idmonoidhom0 (A.1, A.2.1) (B.1, B.2.1) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f
      = lemma_idmonoidhom1 (A.1, A.2.1) (B.1, B.2.1) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = lemma_monoidcomp0 (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) (D.1, D.2.1) f g h

-- Category of Abelian Groups
Ab: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = abgroup
    Hom (A B: Ob): U = abgrouphom A B
    id (A: Ob): Hom A A = idmonoidhom (A.1, A.2.1.1)
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C
      = monoidhomcomp (A.1, A.2.1.1) (B.1, B.2.1.1) (C.1, C.2.1.1) f g
    HomSet (A B: Ob): isSet (Hom A B) = setmonoidhom (A.1,A.2.1.1) (B.1,B.2.1.1)
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f
      = lemma_idmonoidhom0 (A.1, A.2.1.1) (B.1, B.2.1.1) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f
      = lemma_idmonoidhom1 (A.1, A.2.1.1) (B.1, B.2.1.1) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = lemma_monoidcomp0(A.1,A.2.1.1)(B.1,B.2.1.1)(C.1,C.2.1.1)(D.1,D.2.1.1)f g h

-- Product Category of two Categories
Product (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    x: U = carrier X
    y: U = carrier Y
    Ob: U = prod x y
    Hom (A B: Ob): U = prod (id x) (id y)
    id (A: Ob): Hom A A = (idfun x, idfun y)
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = (o x x x f.1 g.1, o y y y f.2 g.2)
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = refl (Hom A D) (c A C D (c A B C f g) h)

-- 3-Category with modifications between natural transformations as 3-hom morphisms
modification (C D: precategory) (F G: catfunctor C D) (I J: ntrans C D F G): U = undefined
Hom3Cat (X Y: precategory) (F G: catfunctor X Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = ntrans X Y F G
    Hom (A B: Ob): U = modification X Y F G A B
    id (A: Ob): Hom A A = undefined
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = undefined
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h)) = undefined

Bicategory (X Y: precategory): precategory = Product Cat (Func X Y)
Tricategory (X Y: precategory) (F G: catfunctor X Y): precategory = Product (Bicategory X Y) (Hom3Cat X Y F G)

bifunctor (C D E: precategory): U = catfunctor (Product C D) E
opx (L A R B: precategory) (F: catfunctor L A) (G: catfunctor R B)
 : catfunctor (Product L R) (Product A B) = undefined

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

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)
     * unit --- ...

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,
            tt ) -- ...

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 = \(a:X->Y)->\(x:X)->(g(f(a)))x
     HomSet (A B: Ob): isSet (Hom A B) = setFun Ob Ob (setFun X Y Z)
     L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f
     R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f
     Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = refl (Hom A D) (c A C D (c A B C f g) h)

reduce (AC BC AB: precategory)
       (H: bifunctor BC AB AC)
       (L: precategory) (F: catfunctor L BC)
       (R: precategory) (G: catfunctor R AB)
     : bifunctor L R AC
     = compFunctor (Product L R) (Product BC AB) AC (opx L BC R AB F G) H

c2impl (Ob: U) (Hom: (A B: Ob) -> precategory)
       (c: (A B C: Ob) -> bifunctor (Hom B C) (Hom A B) (Hom A C))
       (A B C: Ob) (L R: precategory)
       (F: catfunctor L (Hom B C))
       (G: catfunctor R (Hom A B))
     : bifunctor L R (Hom A C)
     = reduce (Hom A C) (Hom B C) (Hom A B) (c A B C) L F R G