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
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  
   id-t1 : Arrow  
   arrow-f :  Arrow
   arrow-g :  Arrow


-- arrow composition

twocomp : {c₁  c₂ : Level } ->  { a b c : TwoObject {c₁} } ->  Arrow  { c₂ }  ->  Arrow  { c₂ }  ->  Maybe ( Arrow  { c₂ }  )
twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-f  = just arrow-f
twocomp {_} {_} {t0} {t1} {t1} id-t1  arrow-g  = just arrow-g
twocomp {_} {_} {t1} {t1} {t1} id-t1  id-t1  = just id-t1
twocomp {_} {_} {t0} {t0} {t1} arrow-f  id-t0 = just arrow-f
twocomp {_} {_} {t0} {t0} {t1} arrow-g  id-t0 = just arrow-g
twocomp {_} {_} {t0} {t0} {t0} id-t0  id-t0 = just id-t0
twocomp _ _ = nothing

_×_ :  { c₁  c₂ : Level }  -> {A B C : TwoObject { c₁} } →  Maybe ( Arrow   { c₂ }) →  Maybe ( Arrow    { c₂ })  →  Maybe ( Arrow  { c₂ })  
_×_   nothing _  = nothing
_×_   _ nothing  = nothing
_×_   { c₁} { c₂} {a} {b} {c} (just f)  (just g)   =  twocomp  { c₁} { c₂} {a} {b} {c} f g  


[_==_] : { c₁ c₂ : Level}   {a b : TwoObject {c₁} } ->  Rel (Maybe (Arrow  { c₂ })) (c₂) 
[_==_]   =  Eq   _≡_ 

--          f    g    h
--       d <- c <- b <- a

assoc-× :   { c₁  c₂ : Level } {a b c d : TwoObject  { c₁} } {f g h : Maybe (Arrow  { c₂ })} → 
   [ f × (g × h) == (f × g) × h ]
assoc-× {_} {_} {_} {_} {_} {_} {nothing} {_} {_} = nothing
assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = nothing
assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} with ((just g ) × (just h)) | ((just f ) × (just g)  )
... | nothing | _ = nothing
... | just _ | nothing = nothing
... | just id-t0 | just id-t0 = just refl
... | just id-t1 | just id-t1 = just refl
... | just id-t1 | just arrow-f = just refl
... | just id-t1 | just arrow-g = just refl
... | just arrow-f | just id-t0  = just refl
... | just arrow-g | just id-t0  = just refl
... | just id-t0 | just id-t1 = nothing
... | just id-t0 | (just arrow-f) = nothing
... | just id-t0 | (just arrow-g) = nothing
... | just id-t1 | (just id-t0) = nothing
... | just arrow-f | (just id-t1) = nothing
... | just arrow-f | (just arrow-f) = nothing
... | just arrow-f | (just arrow-g) = nothing
... | just arrow-g | (just id-t1) = nothing
... | just arrow-g | (just arrow-f) = nothing
... | just arrow-g | (just arrow-g) = nothing

TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (Arrow  { c₂ })
TwoId {_} {_} {t0} = just id-t0
TwoId {_} {_} {t1} = just id-t1


open import maybeCat  


open import Relation.Binary 
TwoCat : { c₁ c₂ ℓ : Level  } ->  Category   c₁  c₂  c₂
TwoCat   {c₁}  {c₂} {ℓ} = record {
    Obj  = TwoObject  {c₁} ;
    Hom = λ a b →    Maybe ( Arrow  { c₂ } ) ;
    _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
    _≈_ =    Eq  _≡_   ;
    Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
    isCategory  = record {
            isEquivalence =  record {refl = {!!}  ; trans = {!!}  ; sym = {!!}  } ;
            identityL  = {!!} ;
            identityR  = {!!} ;
            o-resp-≈  =  {!!} ;
            associative  = {!!}
       } 
   } 

indexFunctor :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj (MaybeCat A )) ( f g : Hom A a b ) ->  Functor (TwoCat {c₁} {c₂} {c₂} ) (MaybeCat 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
          I = TwoCat  {c₁} {c₂} {ℓ}
          MA = MaybeCat A
          open ≈-Reasoning (MA)
          fobj :  Obj I -> Obj A
          fobj t0 = a
          fobj t1 = b
          fmap :  {x y : Obj I } ->  Maybe (Arrow  {c₂} ) -> Hom MA (fobj x) (fobj y)
          fmap {t0} {t1} (just arrow-f) = record { hom = just f }
          fmap {t0} {t1} (just arrow-g) = record { hom = just g }
          fmap {t0} {t0} (just id-t0)  = record { hom = just ( id1 A a )}
          fmap {t1} {t1} (just id-t1)  = record { hom = just ( id1 A b )}
          fmap {_} {_}   _ = record { hom = nothing }
          open ≈-Reasoning (A) 
          identity :  {x : Obj I} → {!!}
          identity {t0}  =  {!!}
          identity {t1}  =  {!!}
          distr1 : {a₁ : Obj I} {b₁ : Obj I} {c : Obj I} {f₁ : Hom I a₁ b₁} {g₁ : Hom I b₁ c} → {!!}
          distr1 {a1} {b1} {c} {f1} {g1}   = {!!}
          ≈-cong :   {a : Obj I} {b : Obj I} {f g : Hom I a b}  → _[_≈_] I f g → {!!}
          ≈-cong   {_} {_} {f1} {g1} f≈g = {!!}


---  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}      (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}  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₂} {ℓ }
         Γ = {!!}
         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 = {!!}