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

open import Data.Nat hiding ( _⊔_ ) renaming ( suc to succ )
open import Data.Bool


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


infixr 40 _::_
data  List {a} (A : Set a)  : Set a where
   [] : List A
   _::_ : A -> List A -> List A

nat-equal : ℕ -> ℕ -> Bool
nat-equal zero zero = true
nat-equal (succ _) zero = false
nat-equal zero (succ _) = false
nat-equal (succ x) (succ y) = nat-equal x y

memberp :  ℕ  ->  List  ℕ  → Bool
memberp _ []  = false
memberp x (y :: T) with nat-equal x y
... | true = true
... | false = memberp x T

memberp1 :  ℕ  ->  List  ℕ  → Bool
memberp1 _ []  = false
memberp1 x (y :: T) with compare x y
memberp1 x (.x :: T)  | equal .x = true
memberp1 x ( .(succ (x + y)) :: T)  | less .x y = memberp1 x T
memberp1 .(succ (x + y)) ( x :: T)  | greater .x y = memberp1 x T


-- Category object configuration

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

two-equality : Two -> Two -> Bool
two-equality  t0 t0 = true
two-equality  t0 t1 = false
two-equality  t1 t0 = true
two-equality  t1 t1 = false

data Arrow  : Set  c₂ where
    id-0 : Arrow
    id-1 :  Arrow
    af :  Arrow
    ag :  Arrow

arrow-equality : Arrow -> Arrow -> Bool
arrow-equality id-0 id-0 = true
arrow-equality id-0 id-1 = false
arrow-equality id-0 af = false
arrow-equality id-0 ag = false
arrow-equality id-1 id-0 = false
arrow-equality id-1 id-1 = true
arrow-equality id-1 af = false
arrow-equality id-1 ag = false
arrow-equality af id-0 = false
arrow-equality af id-1 = false
arrow-equality af af = true
arrow-equality af ag = false
arrow-equality ag id-0 = false
arrow-equality ag id-1 = false
arrow-equality ag af = false
arrow-equality ag ag = true

-- Category arrow configuration

hom : Two  → Two  → List (Arrow )
hom t0 t0 =  id-0 :: []
hom t0 t1 =  af :: ag :: []
hom t1 t0 =  []
hom t1 t1 =  id-1 :: []

in-hom : Arrow -> List Arrow -> Bool
in-hom _ [] = false
in-hom x (y :: T) with arrow-equality  x y
in-hom _ (y :: T) | true = true
in-hom x (y :: T) | false = in-hom x T

record Two-Hom (a : Two  ) (b : Two  ) : Set (c₁ ⊔ suc c₂ ⊔ ℓ) where
   field
       Map    : Arrow 
       isMap  : in-hom  Map ( hom a b )  ≡ true

Two-id :  (a : Two ) ->  Two-Hom a a
Two-id t0  = record { Map = id-0 ; isMap = refl }
Two-id t1  = record { Map = id-1 ; isMap = refl }

open Two-Hom

twocat :  Category c₁ _ (ℓ ⊔ (suc c₂ ⊔ c₁))
twocat  = record {
    Obj  = Two ;
    Hom = λ a b →  Two-Hom a b   ; 
    _o_ =  {!!} ;
    _≈_ = _≡_;
    Id  =  \{a} -> Two-id a ;
    isCategory  = record {
            isEquivalence = {!!} ;
            identityL  = {!!} ;
            identityR  = {!!} ;
            o-resp-≈  = {!!} ;
            associative  = {!!}
       } 
   } where

open Limit

lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
      (two : {!!}  ) 
      (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 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
         Γobj :  Two  → Obj A
         Γobj t0 = a
         Γobj t1 = b
         Γmap :  Two  → Hom A a b
         Γmap t0 = f
         Γmap t1 = g
         Γ : Functor I A
         Γ = record {
            FObj  = λ x → Γobj {!!} ;
            FMap  = λ f → {!!} ;
            isFunctor = record {
                     ≈-cong  = {!!} ; 
                    identity = {!!} ;
                    distr = {!!}
            }
          }
         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)