open import Category -- https://github.com/konn/category-agda
open import Level

module limit-to where

open import cat-utility
open import HomReasoning
open import Relation.Binary.Core

open import discrete


---  Equalizer  from Limit ( 2->A functor Γ and  Nat :  K ->　Γ)
---
---
---                     f
---          e       -----→
---     c -----→  a         b     A
---     ^      /     -----→
---     |k   h          g
---     |   /
---     |  /            ^
---     | /             |
---     |/              | Γ
---     d _             |
---      |\             |
---        \ K          af
---         \       -----→
---          \    t0        t1    I
---                  -----→
---                     ag
---
---

open Complete
open Limit
open NTrans

-- Functor Γ : TwoCat -> A

IndexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat  {c₁} {c₂}) A
IndexFunctor  {c₁} {c₂} {ℓ} A a b f g = record {
         FObj = λ a → fobj a
       ; FMap = λ {a} {b} f → fmap {a} {b} f
       ; isFunctor = record {
             identity = λ{x} → identity x
             ; distr = λ {a} {b} {c} {f} {g}   → distr1 {a} {b} {c} {f} {g}
             ; ≈-cong = λ {a} {b} {c} {f}   → ≈-cong  {a} {b} {c} {f}
       }
      } where
          T = TwoCat   {c₁} {c₂}
          fobj :  Obj T → Obj A
          fobj t0 = a
          fobj t1 = b
          fmap :  {x y : Obj T } →  (Hom T x y  ) → Hom A (fobj x) (fobj y)
          fmap  {t0} {t0} id-t0 = id1 A a
          fmap  {t1} {t1} id-t1 = id1 A b
          fmap  {t0} {t1} arrow-f = f
          fmap  {t0} {t1} arrow-g = g
          ≈-cong :  {a : Obj T} {b : Obj T} {f g : Hom T a b}  → T [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
          ≈-cong  {a} {b} {f} {.f} refl = let open  ≈-Reasoning A in refl-hom
          identity : (x : Obj T ) ->  A [ fmap (id1 T x) ≈  id1 A (fobj x) ]
          identity t0  = let open  ≈-Reasoning A in refl-hom
          identity t1  = let open  ≈-Reasoning A in refl-hom
          distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} →
               A [ fmap (T [ g o f ])  ≈  A [ fmap g o fmap f ] ]
          distr1  {t0} {t0} {t0} {id-t0 } { id-t0 } = let open  ≈-Reasoning A in sym-hom idL
          distr1  {t1} {t1} {t1} { id-t1 } { id-t1 } = let open  ≈-Reasoning A in begin
                   id b
                ≈↑⟨ idL ⟩
                   id b o id b
                ∎
          distr1  {t0} {t0} {t1} { id-t0 } { arrow-f } = let open  ≈-Reasoning A in begin
                  fmap (T [ arrow-f  o id-t0 ] )
                ≈⟨⟩
                  fmap arrow-f
                ≈↑⟨ idR ⟩
                   fmap arrow-f o id a
                ∎
          distr1  {t0} {t0} {t1}  { id-t0 } { arrow-g } = let open  ≈-Reasoning A in begin
                  fmap (T [ arrow-g  o id-t0 ] )
                ≈⟨⟩
                  fmap arrow-g
                ≈↑⟨ idR ⟩
                   fmap arrow-g o id a
                ∎
          distr1  {t0} {t1} {t1}  { arrow-f } { id-t1 } = let open  ≈-Reasoning A in begin
                  fmap (T [ id-t1  o arrow-f ] )
                ≈⟨⟩
                  fmap arrow-f
                ≈↑⟨ idL ⟩
                   id b o  fmap arrow-f
                ∎
          distr1  {t0} {t1} {t1} { arrow-g } { id-t1 } = let open  ≈-Reasoning A in begin
                  fmap (T [ id-t1  o arrow-g ] )
                ≈⟨⟩
                  fmap arrow-g
                ≈↑⟨ idL ⟩
                   id b o  fmap arrow-g
                ∎

--- Nat for Limit
--
--     Nat : K -> IndexFunctor
--

open Functor

IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
        →  {a b : Obj A}      (f g : Hom A  a b )
    (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   →
        NTrans TwoCat  A (K A TwoCat  d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
    TMap = λ x → nmap x d h ;
    isNTrans = record {
        commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh
    }
 } where
         I = TwoCat  {c₁} {c₂}
         Γ : Functor I A
         Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
         nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
         nmap t0 d h = h
         nmap t1 d h = A [ f o  h ]
         commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
         commute1  {t0} {t1} {arrow-f}  d h fh=gh =  let open  ≈-Reasoning A in begin
                    f o h
                ≈↑⟨ idR ⟩
                    (f o h ) o id d
                ∎
         commute1  {t0} {t1} {arrow-g}  d h fh=gh =  let open  ≈-Reasoning A in begin
                    g o h
                ≈↑⟨ fh=gh ⟩
                    f o h
                ≈↑⟨ idR ⟩
                    (f o h ) o id d
                ∎
         commute1  {t0} {t0} {id-t0}  d h fh=gh =   let open  ≈-Reasoning A in begin
                    id a o h
                ≈⟨ idL ⟩
                    h
                ≈↑⟨ idR ⟩
                    h o id d
                ∎
         commute1  {t1} {t1} {id-t1}  d h fh=gh =   let open  ≈-Reasoning A in begin
                    id b o  ( f o  h  )
                ≈⟨ idL ⟩
                     f o  h
                ≈↑⟨ idR ⟩
                    ( f o  h ) o id d
                ∎


equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A TwoCat ) ->
         Hom A ( limit-c comp (IndexFunctor A a b f g)) a
equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0

lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (comp : Complete A TwoCat  )
        →  {a b : Obj A}  (f g : Hom A  a b )
        → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] )
        → IsEqualizer A (equlimit A f g comp) f g
lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge =  record {
        fe=ge =  fe=ge
        ; k = λ {d} h fh=gh → k {d} h fh=gh
        ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh
        ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k'
     } where
         I : Category  c₁ c₂ c₂
         I = TwoCat
         Γ : Functor I A
         Γ = IndexFunctor A a b f g
         e : Hom A (limit-c comp (IndexFunctor A a b f g)) a
         e = equlimit A f g comp
         c : Obj A
         c = limit-c comp Γ
         lim : Limit A I Γ c ( limit-u comp Γ )
         lim =  isLimit comp  Γ
         inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
         inat = IndexNat A f g
         k : {d : Obj A}  (h : Hom A d a) → A [ A [ f  o  h ] ≈ A [ g  o h ] ] → Hom A d c
         k {d} h fh=gh  =  limit lim d (inat d h fh=gh )
         ek=h :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  → A [ A [ e o k h fh=gh ] ≈ h ]
         ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
                    e o k h fh=gh
                ≈⟨⟩
                    TMap (limit-u comp Γ) t0  o k h fh=gh
                ≈⟨ t0f=t lim {d} {inat d h fh=gh } {t0}  ⟩
                    TMap (inat d h fh=gh) t0
                ≈⟨⟩
                    h
                ∎
         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c )
                       ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →
                       A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ]
         uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
                    TMap (limit-u comp Γ) t0 o k'
                ≈⟨⟩
                    e o k'
                ≈⟨ ek'=h ⟩
                    h
                ≈⟨⟩
                    TMap (inat d h fh=gh) t0
                ∎
         uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
                    TMap (limit-u comp Γ) t1 o k'
                ≈↑⟨ car (idR) ⟩
                    ( TMap (limit-u comp Γ) t1  o  id c ) o k'
                ≈⟨⟩
                    ( TMap (limit-u comp Γ) t1  o  FMap (K A I c) arrow-f ) o k'
                ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
                    ( FMap Γ  arrow-f  o TMap (limit-u comp Γ) t0 ) o k'
                ≈⟨⟩
                   (f o e ) o k'
                ≈↑⟨ assoc ⟩
                   f o ( e o k' )
                ≈⟨ cdr  ek'=h ⟩
                    f o h
                ≈⟨⟩
                    TMap (inat d h fh=gh) t1
                ∎
         uniquness :  (d : Obj A ) (h : Hom A d a ) →  ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ] )  →
                 ( k' : Hom A d c )
                → A [ A [ e o k' ] ≈ h ] → A [ k h  fh=gh   ≈ k' ]
         uniquness d h fh=gh k' ek'=h =  let open  ≈-Reasoning A in  begin
                    k h fh=gh
                ≈⟨ limit-uniqueness lim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
                    k'
                ∎


plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) )  
      →  ( Γ : Functor (DiscreteCat {c₁}) A ) → Obj A
plimit A comp Γ = limit-c comp Γ

pnat :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A ( DiscreteCat {c₁} ) ) 
    → (Γ : Functor (DiscreteCat {c₁}) A )
    →  (q : Obj A )  ( qi : (i : Obj ( DiscreteCat {c₁} )) → Hom A q (FObj Γ i) )
    → NTrans DiscreteCat A (K A DiscreteCat q) Γ
pnat {c₁} A comp Γ q qi  = record {
        TMap = qi ; 
        isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
    } where
        commute :  {a b : Obj (DiscreteCat {c₁}) } {f : Hom ( DiscreteCat {c₁})  a b} →
                A [ A [ FMap Γ f o qi a ] ≈
                A [ qi  b o FMap (K A (DiscreteCat {c₁} )q) f ] ]
        commute {a} {b} {f} =  let open  ≈-Reasoning A in  begin
                  FMap Γ f o qi a
                ≈⟨⟩
                  FMap Γ (id1 (DiscreteCat {c₁}) b ) o qi a
                ≈⟨ car ( IsFunctor.identity  ( isFunctor Γ  )) ⟩
                 id (FObj Γ b)  o qi a
                ≈⟨ idL ⟩
                   qi  a 
                ≈⟨⟩  -- only a = b case in discrete category
                   qi  b 
                ≈↑⟨ idR ⟩
                   qi  b o id q
                ≈⟨⟩
                   qi  b o FMap (K A (DiscreteCat {c₁} )q) f
                ∎

lim-to-product :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
      (comp : Complete A ( DiscreteCat {c₁} ) )
        →  ( Γ : Functor (DiscreteCat {c₁}) A )  
        → IProduct {c₁} A (Obj ( DiscreteCat {c₁}) )(plimit A comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u  comp Γ) i )
lim-to-product {c₁} A comp Γ = record {
              iproduct = λ {q} qi → iproduct {q} qi ;
              pif=q =  λ {q } qi { i } → pif=q {q} qi {i}  ;
              ip-uniqueness  = λ  {q } { h } → ip-uniqueness {q} {h} ;
              ip-cong  =  λ {q } { qi }  { qi' } qi=qi' → ip-cong  {q} {qi} {qi'} qi=qi'
   } where
        D =  DiscreteCat {c₁} 
        I = Obj ( DiscreteCat {c₁} )
        lim = isLimit comp Γ
        ai = λ i → FObj Γ i
        p = limit-c comp Γ
        pi =  λ i → TMap (limit-u  comp Γ) i
        iproduct : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
        iproduct {q} qi = limit lim q (pnat A comp Γ q qi )
        pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( iproduct qi ) ] ≈  (qi i) ]
        pif=q {q} qi {i} = t0f=t lim  {q} {pnat A comp Γ q qi } {i}
        ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ]
        ipu {i} q h = let open  ≈-Reasoning A in  refl-hom
        ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
        ip-uniqueness {q} {h} = limit-uniqueness lim {q} {pnat A comp Γ q (λ i → A [ pi i  o h ]  )} h (ipu q h)
        ipc : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 
             → (i : I ) →  A [ qi i ≈ qi' i ]  → 
             A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A comp Γ q qi) i ]
        ipc {q} {qi} {qi'} i qi=qi' = let open  ≈-Reasoning A in begin
                  TMap (limit-u comp Γ) i o iproduct qi' 
                ≈⟨⟩
                  TMap (limit-u comp Γ) i o limit lim q (pnat A comp Γ q qi' )
                ≈⟨ t0f=t lim {q} {pnat A comp Γ q qi'} {i} ⟩
                  TMap (pnat A comp Γ q qi') i
                ≈⟨⟩
                  qi' i
                ≈↑⟨ qi=qi' ⟩
                  qi i
                ≈⟨⟩
                  TMap (pnat A comp Γ q qi) i
                ∎
        ip-cong : {q : Obj A}   → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
                        → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
        ip-cong {q} {qi} {qi'} qi=qi' =  limit-uniqueness lim {q} {pnat A comp Γ q qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))