{- Category Theory:
   - Natural Transformations;
   - Kan Extensions;
   - Limits;
   - Adjunctions.
   Copyright (c) Groupoid Infinity, 2017-2018.

   HoTT 9.3 Adjunctions. -}

module adj where
import cat
import fun

unitCat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = unit
    Hom (A B: Ob): U = unit
    id (A: Ob): Hom A A = tt
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = tt
    HomSet (A B: Ob): isSet (Hom A B) = setUnit
    L (A B: Ob): (f: unit) -> Path unit (c A A B (id A) f) f = split tt -> <i> tt
    R (A B: Ob): (f: unit) -> Path unit (c A B B f (id B)) f = split tt -> <i> tt
    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 unit tt

isNaturalTrans (C D: precategory)
               (F G: catfunctor C D)
               (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x)): U
  = (x y: carrier C) (h: hom C x y) ->
    Path (hom D (F.1 x) (G.1 y))
         (compose D (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (eta y))
         (compose D (F.1 x) (G.1 x) (G.1 y) (eta x) (G.2.1 x y h))

-- Awodey CT 7.6. Natural transformation
-- Natural Transformation
ntrans (C D: precategory) (F G: catfunctor C D): U
    = (eta: (x: carrier C) -> hom D (F.1 x) (G.1 x))
    * (isNaturalTrans C D F G eta)

-- Kan Extensions
extension (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U
    = (F: catfunctor B C)
    * (counit: ntrans A C (compFunctor A B C K F) G)
    * unit

-- Functor to Unit Category
unitFunc (C: precategory): catfunctor C unitCat
    = undefined

-- Cone as Kan Extension
cone (J C: precategory) (D: catfunctor J C): U
   = extension J unitCat C (unitFunc J) D

-- universality of Kan Extension
universality (A B C: precategory)
             (K: catfunctor A B) (G: catfunctor A C)
             (s t: extension A B C K G) : U
           = undefined

-- Right Kan Extension
ran   (A B C: precategory) (K: catfunctor A B) (G: catfunctor A C) : U
    = (x: extension A B C K G) * ((y: extension A B C K G)
    -> isContr (universality A B C K G x y))

-- Limit
limit (J C: precategory) (D: catfunctor J C): U
    = ran J unitCat C (unitFunc J) D

-- ExtUniv : Extension K G → Set _
-- ExtUniv (extension S (nt α _)) = Σ (S ⇒ F) λ { (nt β _) → (∀ X → ε X ∘ β (apply K X) ≡ α X) }

ntransL (C D: precategory) (F G: catfunctor C D) (f: ntrans C D F G) (B: precategory) (H: catfunctor B C)
      : ntrans B D (compFunctor B C D H F) (compFunctor B C D H G)
      = (eta, p) where
        F': catfunctor B D = compFunctor B C D H F
        G': catfunctor B D = compFunctor B C D H G
        eta (x: carrier B): hom D (F'.1 x) (G'.1 x) = f.1 (H.1 x)
        p (x y: carrier B) (h: hom B x y): Path (hom D (F'.1 x) (G'.1 y))
            (compose D (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y))
            (compose D (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h))
          = f.2 (H.1 x) (H.1 y) (H.2.1 x y h)

ntransR (C D: precategory) (F G: catfunctor C D) (f: ntrans C D F G) (E: precategory) (H: catfunctor D E)
  : ntrans C E (compFunctor C D E F H) (compFunctor C D E G H)
  = (eta, p) where
    F': catfunctor C E = compFunctor C D E F H
    G': catfunctor C E = compFunctor C D E G H
    eta (x: carrier C): hom E (F'.1 x) (G'.1 x) = H.2.1 (F.1 x) (G.1 x) (f.1 x)
    p (x y: carrier C) (h: hom C x y): Path (hom E (F'.1 x) (G'.1 y))
        (compose E (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y))
        (compose E (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h))
      = <i> comp (<_> hom E (F'.1 x) (G'.1 y)) (H.2.1 (F.1 x) (G.1 y) (f.2 x y h @ i))
        [ (i = 0) -> H.2.2.2 (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (f.1 y),
          (i = 1) -> H.2.2.2 (F.1 x) (G.1 x) (G.1 y) (f.1 x) (G.2.1 x y h) ]

hom3 (C D: precategory)
     (F: catfunctor C D)
     (G: catfunctor C D)
     (left: ntrans C D F G)
     (right: ntrans C D F G): U = undefined

-- Adjointness Property
-- NOTE: Adjunction is a special case of signature class of 3-morphisms
areAdjoint (C D: precategory)
           (F: catfunctor D C)
           (G: catfunctor C D)
           (unit: ntrans D D (idFunctor D) (compFunctor D C D F G))
           (counit: ntrans C C (compFunctor C D C G F) (idFunctor C)): U
  = prod  ((x: carrier C) -> Path (hom D (G.1 x) (G.1 x)) (path D (G.1 x)) (h0 x))
          ((x: carrier D) -> Path (hom C (F.1 x) (F.1 x)) (path C (F.1 x)) (h1 x)) where
    h0 (x:  carrier C) : hom D (G.1 x) (G.1 x) = compose D (G.1 x) (G.1 (F.1 (G.1 x))) (G.1 x)
          ((ntransL D D (idFunctor D) (compFunctor D C D F G) unit C G).1 x)
          ((ntransR C C (compFunctor C D C G F) (idFunctor C) counit D G).1 x)
    h1 (x:  carrier D) : hom C (F.1 x) (F.1 x) = compose C (F.1 x) (F.1 (G.1 (F.1 x))) (F.1 x)
          ((ntransR D D (idFunctor D) (compFunctor D C D F G) unit C F).1 x)
          ((ntransL C C (compFunctor C D C G F) (idFunctor C) counit D F).1 x)

-- Adjoint of two Natural Transformations
adjoint (C D: precategory) (F: catfunctor D C) (G: catfunctor C D): U
  = (unit: ntrans D D (idFunctor D) (compFunctor D C D F G))
  * (counit: ntrans C C (compFunctor C D C G F) (idFunctor C))
  * areAdjoint C D F G unit counit