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 Functor



-- If we have limit then we have equalizer
---  two objects category
---
---    t0    f    t1
---       -----→
---                
---       -----→
---    t2    g    t3



data  Object4 {c₁ : Level}  : Set c₁ where
   t0 : Object4
   t1 : Object4
   t2 : Object4
   t3 : Object4

record TwoHom {c₁ : Level} {Object : Set c₁}   (a b : Object) : Set c₁ where

open TwoHom

-- arrow composition


_×_ :  ∀ {c₁ }  → { Object : Set  c₁} → {a b c : Object } →  ( TwoHom {c₁} {Object} b c ) →  ( TwoHom {c₁}  {Object} a b )  
    →  ( TwoHom {c₁}  {Object} a c )
_×_  {c₁}  {Object} {a} {b} {c} f g  = record { }



TwoId :  {c₁ : Level } {Object : Set c₁} (a : Object   ) →  (TwoHom {c₁}   {Object} a a )
TwoId {_} a = record { }


open import Relation.Binary
TwoCat : {c₁ : Level  } →  (Object : Set  c₁) → Category   c₁ c₁ c₁ 
TwoCat   {c₁} Object = record {
    Obj  = Object   ;
    Hom = λ a b →    ( TwoHom {c₁}  {Object} a b ) ;
    _o_ =  λ{a} {b} {c} x y → _×_ {c₁ }  {Object} {a} {b} {c} x y ;
    _≈_ =  λ x y → x ≡ y ;
    Id  =  λ{a} → TwoId {c₁ } {Object} a ;
    isCategory  = record {
            isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} ;
            identityL  = λ{a b f} → identityL {a} {b} {f} ;
            identityR  = λ{a b f} → identityR {a} {b} {f} ;
            o-resp-≈  = λ{a b c f g h i} →  o-resp-≈  {a} {b} {c} {f} {g} {h} {i} ;
            associative  = λ{a b c d f g h } → assoc-×      {a} {b} {c} {d} {f} {g} {h}
       }
   }  where
        identityL :   {A B : Object } {f : ( TwoHom {c₁} {Object}  A B) } →  ((TwoId {_} {Object} B)  × f)   ≡  f
        identityL =  refl
        identityR :  {A B : Object } {f : ( TwoHom {_}  {Object} A B) } →   ( f × TwoId A )   ≡  f
        identityR = refl
        o-resp-≈ :   {A B C : Object  } {f g :  ( TwoHom {c₁}  {Object} A B)} {h i : ( TwoHom B C)} →
            f  ≡  g → h  ≡  i → ( h × f )  ≡  ( i × g )
        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  refl refl  = refl
        assoc-× :    {a b c d : Object  }
               {f : (TwoHom {c₁}   {Object} c d )} →
               {g : (TwoHom {c₁}   {Object} b c )} →
               {h : (TwoHom {c₁}   {Object} a b )} →
               ( f × (g × h)) ≡ ((f × g) × h )
        assoc-×  {a} {b} {c} {d} {f} {g} {h} = refl



record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where
     field 
         nil : {a b : Obj A } → Hom A a b
         nil-id : {a  : Obj A } →  A [ nil {a} {a} ≈ id1 A a ]    -- too strong but we need this
         nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ]   ≈ nil {a} {c} ]
         nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ]   ≈ nil {a} {c} ]

open Nil



indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) →  Functor (TwoCat {c₁} Object4 ) A
indexFunctor  {c₁} {c₂} {ℓ} A none 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
          I = TwoCat  {c₁}  Object4
          fobj :  Obj I → Obj A
          fobj t0 = a
          fobj t1 = b
          fobj t2 = a
          fobj t3 = b
          fmap :  {x y : Obj I } →  (TwoHom {c₁}  {Object4} x y  ) → Hom A (fobj x) (fobj y)
          fmap  {t0} {t0} h  = id1 A a
          fmap  {t1} {t1} h  = id1 A b
          fmap  {t2} {t2} h  = id1 A a
          fmap  {t3} {t3} h  = id1 A b
          fmap  {t0} {t1} h  = f
          fmap  {t2} {t3} h  = g
          fmap  {_} {_} h  =  nil none
          open  ≈-Reasoning A
          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ]  → A [ fmap f ≈ fmap g ]
          ≈-cong   {a} {b} {f1} {g1} f≈g = refl-hom
          identity :  {x : Obj I} → A [ fmap ( id1 I x ) ≈  id1 A (fobj x) ]
          identity {t0} = refl-hom
          identity {t1} = refl-hom
          identity {t2} = refl-hom
          identity {t3} = refl-hom
          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} →
               A [ fmap (I [ g₁ o f₁ ])  ≈  A [ fmap g₁ o fmap f₁ ] ]
          distr1 {t0} {t0} {t0} {f1} {g1}   = begin
                    id1 A a
                ≈↑⟨ idL ⟩
                    A [ id1 A a  o id1 A a ]
                ∎
          distr1 {t1} {t1} {t1} {f1} {g1}   = sym idL
          distr1 {t2} {t2} {t2} {f1} {g1}   = sym idL
          distr1 {t3} {t3} {t3} {f1} {g1}   = sym idL
          distr1 {t0} {t1} {t1} {f1} {g1}   = sym idL
          distr1 {t0} {t1} {_} {f1} {g1}   = ?
          distr1 {a1} {b1} {c1} {f1} {g1}   = {!!}

---  Equalizer
---                     f
---          e       -----→
---     c -----→  a         b
---     ^      /     -----→
---     |k   h          g
---     |   /
---     |  /            ^
---     | /             |
---     |/              | Γ
---     d _             |
---      |\             |
---        \ K          af
---         \        -----→
---          \     t0        t1
---                  -----→
---                     ag
---      
---      

open Limit

I' :  {c₁ : Level} →  Category   c₁ c₁   c₁  
I' {c₁}  = TwoCat {c₁} Object4

lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( none : Nil A )
      (lim :  ( Γ : Functor (I' {c₁} ) A ) → {a0 : Obj A } 
               {u : NTrans I' A ( K A  I' a0 )  Γ } → Limit A I' Γ a0 u ) -- completeness
        →  {a b c : Obj A}      (f g : Hom A  a b )
        → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → IsEqualizer A e f g
lim-to-equ  {c₁} {c₂} {ℓ } A none  lim {a} {b} {c}  f g e 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
         open  ≈-Reasoning A
         I : Category c₁ c₁  c₁ 
         I = I'   {c₁} 
         Γ : Functor I A
         Γ = indexFunctor  {c₁} {c₂} {ℓ} A  none 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 x d 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 = {!!}
         nat1 : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
         nat1 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 
            }
          }
         eqlim = lim Γ  {c} {nat1 c e fe=ge }
         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 eqlim d (nat1 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 =   begin
                    e o k h fh=gh
                ≈⟨ t0f=t eqlim {d} {nat1 d h fh=gh} {t0}  ⟩
                    h
                ∎
         uniq-nat :  {i : Obj I} →  (d : Obj A )  (h : Hom A d a ) ( k' : Hom A d c ) → A [ A [ e o k' ] ≈ h ] → A [ A [ nmap i c e o k' ] ≈ nmap i d h ]
         uniq-nat d h k' ek'=h =  {!!}
         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 =   begin
                    k h fh=gh
                -- ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' ek'=h ) ⟩
                ≈⟨ {!!} ⟩
                    k'
                ∎