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

module limit-to {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
  where

open import cat-utility
open import HomReasoning
open import Relation.Binary.Core
open import Category.Sets
open Functor


-- If we have limit then we have equalizer                                                                                                                                                                  
---  two objects category
---
---          f
---       ------>
---     0         1
---       ------>
---          g

data Two {c₁}  : Set c₁ where
   t0 : Two 
   t1 : Two 

record TwoCat  {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) 
      (two : Two {c₁}) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
       obj  : Two {c₁}  → Obj I
       obj← : Obj I → Two  
       map  : Two {c₁} → Hom I (obj t0) (obj t1) 
       map← : Hom I (obj t0) (obj t1) → Two {c₁}  
       unique-obj  :  ∀{two : Two } → obj← ( obj two ) ≡ two
       unique-obj1 :  ∀{i : Obj I } → obj ( obj← i ) ≡ i
       unique-map  :  ∀{two : Two } → map← ( map two ) ≡ two
       unique-map1 :  ∀{f : Hom I (obj t0) (obj t1) } → map ( map← f ) ≡ f

open Limit
open TwoCat

record two-Γ  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) 
       (a b : Obj A)  (f g : Hom A a b )
       (two : Two) (twocat : TwoCat I two ) (Γ : Functor I A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
    field
       a0  :  FObj Γ (obj twocat t0 ) ≡ a 
       b0  :  FObj Γ (obj twocat t1 ) ≡ b 
       f0  :  A [ FMap Γ (map twocat t0 ) ≈ f ]
       g0  :  A [ FMap Γ (map twocat t0 ) ≈ g ]

lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
      (two : Two  ) 
      (twocat : TwoCat I two) 
      (Γ : Functor I A)
      (lim : ( Γ : Functor I 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 ] ] ) → Equalizer A e f g
lim-to-equ {c₁} A I two twocat Γ 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} → {!!}
        ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!}
     } where
         nat : (d : Obj A) → NTrans I A (K A I d) Γ
         nat d = record {
            TMap = λ x → {!!} ;
            isNTrans = record {
                commute = {!!}
            }
          }
         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 Γ {c} {nat c}) d (nat d)