{- 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

-- Definition (Additive Category).
abcategory: U
  = (X: U) -- group
  * (hom: X -> X -> U) -- abgroup
  * (id: (x: X) -> hom x x)
  * (c: (x y z: X) -> hom x y -> hom y z -> hom x z)
  * (homSet: (x y: X) -> isSet (hom x y))
  * (left1: (x y: X) (f: hom x y) -> Path (hom x y) (c x x y (id x) f) f)
  * (right1: (x y: X) (f: hom x y) -> Path (hom x y) (c x y y f (id y)) f)
  * (assoc: (x y z w: X) (f: hom x y) (g: hom y z) (h: hom z w)
    -> Path (hom x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
  * (z0: X)
  * (zer: (x: X) -> (z: X) * (l: hom z x) * (r: hom x z) * Path X z z0)
  * (mul: X -> X -> X)
  * (sum: X -> X -> X)
  * (pi1: (A B: X) -> hom (mul A B) A)
  * (pi2: (A B: X) -> hom (mul A B) B)
  * (inl: (A B: X) -> hom A (sum A B))
  * (inr: (A B: X) -> hom B (sum A B))
--  * (precomp: (x y z w: X) (f: hom x y) (g: hom y z) (h: hom y w) -> c x y z f (sum )
-- f o (g + h) = f o g + f o h
-- (f + g) o h = f o h + g o h
  * U

--complex (a: abcategory): U
--  = (objects: (n: nat) -> a.1)
--  * (morphisms: (n: nat) -> a.2.1)
--  * ((n: nat) -> Path a.1 (a.2.2.1 (objects n) (objects (succ n)) (objects (succ (succ n)))
--                                   (morphisms (succ n)) (morphisms n)) (a.2.2.2.2.2.2.2.2.1))


instance: abcategory = (Ob,Hom,id,c,homSet,L,R,Q,e,zer,mul,sum,pi1,pi2,inl,inr,Ob) where
    Ob: U = unit
    Hom (x y: Ob): U = abgroup
    id (x: Ob): Hom x x = unitAbGroup
    e: Ob = tt
    c (x y z: Ob) (f g: abgroup): abgroup = unitAbGroup
    homSet (x y: Ob): isSet (abgroup) = undefined
    L (x y: Ob) (f: abgroup): Path (abgroup) (c x x y (id x) f) f = undefined
    R (x y: Ob) (f: abgroup): Path (abgroup) (c x y y f (id y)) f = undefined
    Q (x y z w: Ob) (f g h: abgroup):
      Path (abgroup) (c x z w (c x y z f g) h)
                     (c x y w f (c y z w g h)) = undefined
    zer: (x: Ob) -> (z: Ob) * (l: Hom z x) * (r: Hom x z) * Path Ob z e = undefined
    mul: Ob -> Ob -> Ob = \(x y: Ob) -> tt
    sum: Ob -> Ob -> Ob = \(x y: Ob) -> tt
    pi1: (x y: Ob) -> Hom (mul x y) x = \(x y: Ob) -> unitAbGroup
    pi2: (x y: Ob) -> Hom (mul x y) y = \(x y: Ob) -> unitAbGroup
    inl: (x y: Ob) -> Hom x (mul x y) = \(x y: Ob) -> unitAbGroup
    inr: (x y: Ob) -> Hom y (mul x y) = \(x y: Ob) -> unitAbGroup

-- 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