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 Data.Maybe.Core
open Functor


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



data  TwoObject {c₁ : Level}  : Set c₁ where
   t0 : TwoObject 
   t1 : TwoObject 

data Arrow {ℓ : Level }  : Set ℓ where
   id-t0 : Arrow  
   arrow-f :  Arrow
   arrow-g :  Arrow
   reverse-f :  Arrow
   reverse-g :  Arrow
   nil :  Arrow

record RawHom {c₁ ℓ : Level}  (a : TwoObject {c₁}  ) (b : TwoObject {c₁}  ) : Set  (c₁  ⊔ ℓ) where
   field
       RawMap    : Arrow  {ℓ }

open RawHom

arrow2hom :  {c₁ ℓ : Level}  -> {a : TwoObject {c₁}  } {b : TwoObject {c₁}  } -> Arrow  {ℓ } -> RawHom  { c₁}  {ℓ } a b
arrow2hom id-t0 =  record { RawMap = id-t0 } 
arrow2hom arrow-f =  record { RawMap = arrow-f } 
arrow2hom arrow-g =  record { RawMap = arrow-g } 
arrow2hom reverse-f =  record { RawMap = reverse-f } 
arrow2hom reverse-g =  record { RawMap = reverse-g } 
arrow2hom nil =  record { RawMap = nil } 

record Two-Hom { c₁  ℓ : Level }   (a : TwoObject { c₁}  ) (b : TwoObject  { c₁} ) : Set   (c₁  ⊔ ℓ)  where
   field
      hom : RawHom { c₁}  {ℓ } a b
      arrow-iso : arrow2hom ( RawMap hom )  ≡ hom
   Map : Arrow
   Map = RawMap hom

Two-id :  {c₁ ℓ : Level } -> (a : TwoObject {c₁} ) ->   Two-Hom {c₁} { ℓ} a a 
Two-id _  = record { hom = record { RawMap = id-t0 } ;   arrow-iso = refl }

-- arrow composition

twocomp :  {ℓ : Level } -> Arrow {ℓ } -> Arrow {ℓ } -> Arrow {ℓ } 
twocomp id-t0  f  = f
twocomp f id-t0 = f
twocomp arrow-f reverse-f = id-t0
twocomp arrow-g reverse-g = id-t0
twocomp reverse-f arrow-f = id-t0
twocomp reverse-g arrow-g = id-t0
twocomp _ _ = nil

_×_ :  { c₁  ℓ : Level }  -> {A B C : TwoObject { c₁} } →  Two-Hom { c₁}  {ℓ}  B C →  Two-Hom { c₁}  {ℓ}  A B  →  Two-Hom { c₁}  {ℓ}  A C 
_×_   { c₁} {ℓ} {a} {b} {c} f g  = record { hom =  arrow ;
                    arrow-iso =  arrow-iso   (RawMap arrow  ) }
   where
      arrow  =   arrow2hom {c₁ } {ℓ } {a} {c} ( twocomp  {ℓ} (Two-Hom.Map f) (Two-Hom.Map g)  ) 
      arrow-iso : (f : Arrow { ℓ} ) -> 
             arrow2hom {c₁} {ℓ } {a} {c} f ≡ record { RawMap = f }
      arrow-iso   id-t0 = refl
      arrow-iso  arrow-f = refl
      arrow-iso  arrow-g = refl
      arrow-iso  reverse-f = refl
      arrow-iso  reverse-g = refl
      arrow-iso  nil = refl

open Two-Hom


TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  (ℓ ⊔ c₁)  ℓ
TwoCat   {c₁}  {c₂} {ℓ} = record {
    Obj  = TwoObject  {c₁} ;
    Hom = λ a b →   Two-Hom {c₁ } { ℓ}  a b   ; 
    _o_ =  _×_  { c₁}  {ℓ} ;
    _≈_ = λ a b →   Map a ≡ Map b  ;
    Id  =  \{a} -> Two-id 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 } -> associative  {a} {b} {c} {d} {f} {g} {h}
       } 
   } where
        open  import  Relation.Binary.PropositionalEquality
        ≡-cong = Relation.Binary.PropositionalEquality.cong 
        identityL : {A B : TwoObject} {f : Two-Hom A B} →  Map ( Two-id B × f ) ≡ Map f
        identityL {a} {b} {f} with Map f
        identityL {t0} {t0} {f}  | id-t0 =  refl
        identityL {t1} {t0} {f}  | id-t0 =  refl
        identityL {t0} {t0} {f}  | nil =  refl
        identityL {t0} {t1} {f}  | nil =  refl
        identityL {t1} {t0} {f}  | nil =  refl
        identityL {t1} {t1} {f}  | nil =  refl
        identityL {a} {t1} {f}  | id-t0 =  let open ≡-Reasoning in
              begin
                  {!!}
              ≡⟨ {!!} ⟩
                 id-t0
              ∎
        identityL {_} {_} {f}  | _ =  {!!}

        identityR : {A B : TwoObject} {f : Two-Hom A B} →  Map ( f × Two-id A  ) ≡ Map f
        identityR {a} {b} {f} = {!!}
        o-resp-≈ : {A B C : TwoObject} {f g :  Two-Hom A B} {h i : Two-Hom B C} →
            Map f ≡ Map g → Map h ≡ Map i → Map ( h × f ) ≡ Map ( i × g )
        o-resp-≈  {a} {b} {c} {f} {g} {h} {i}  f≡g h≡i  = let open ≡-Reasoning in
              begin
                 Map (h × f)
              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp (Map h) x ) ) )  f≡g  ⟩
                 Map (h × g)
              ≡⟨  ≡-cong (\x ->  RawMap ( arrow2hom  ( twocomp x (Map g) ) ) )  h≡i  ⟩
                 Map (i × g)
              ∎
        associative : {A B C D : TwoObject} {f : Two-Hom C D} {g : Two-Hom B C} {h : Two-Hom A B} → Map ( f × (g × h) ) ≡ Map ( (f × g) × h )
        associative {_} {_} {_} {_} {f} {g} {h} = {!!}

indexFunctor :  {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ) 
        ( a b : Obj A ) ( f g : Hom A a b )  ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b ) ->  Functor (TwoCat {c₁} {c₂} {ℓ} ) A
indexFunctor  {c₁} {c₂} {ℓ} A a b f g nf nf-rev nidA nidB = record {
         FObj = λ a → fobj a
       ; FMap = λ f → fmap f
       ; isFunctor = record {
             identity = \{x} -> identity {x}
             ; distr = \ {a} {b} {c} {f} {g}   -> distr1 {a} {b} {c} {f} {g} 
             ; ≈-cong = {!!}
       }
      } where
          I = TwoCat  {c₁} {c₂} {ℓ}
          fobj :  Obj I -> Obj A
          fobj t0 = a
          fobj t1 = b
          fmap1 :  {x y : Obj I } -> Hom I x y -> Arrow -> Hom A (fobj x) (fobj y)
          fmap1 {_} {_} x  f = {!!}
          fmap :  {x y : Obj I } -> Hom I x y -> Hom A (fobj x) (fobj y)
          fmap {x} {y} f  = fmap1 {x} {y} f ( Map f)
          open ≈-Reasoning (A) 
          identity :  {x : Obj I} → A [ fmap (id1 I  x) ≈ id1 A  (fobj x) ]
          identity {t0}  =  refl-hom
          identity {t1}  =  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 = {!!}
          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → I [ f ≈ g ] → A [ fmap f ≈ fmap g ]
          ≈-cong   {_} {_} {f1} {g1} f≈g = {!!} -- ≡-cong f≈g (\x -> fmap1 g1 x)     


---  Equalizer
---                     f
---          e       ------>
---     c ------>  a         b
---     ^      /     ------>
---     |k   h          g
---     |   / 
---     |  / 
---     | /  
---     |/  
---     d  

open Limit

lim-to-equ : {c₁ c₂ ℓ : Level}  (A : Category c₁ c₂ ℓ)  
      (lim : (I : Category c₁ c₂ ℓ) ( Γ : 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} ( nf : Hom A a b ) ( nf-rev : Hom A b a ) ( nidA : Hom A a a ) ( nidB : Hom A b b )  (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₁} {c₂} {ℓ } A lim {a} {b} {c} nf nf-rev nidA nidB  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
         I = TwoCat {c₁} {c₂} {ℓ }
         Γ = indexFunctor A a b f g nf nf-rev nidA nidB
         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  {x} {y} {f'} d h fh=gh = {!!}
         nat : (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   → NTrans I A (K A I d) Γ
         nat 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 
            }
          }
         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 I Γ  {c} {nat c e fe=ge }) d (nat 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 = {!!}
         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 = {!!}