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

module freyd1 {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ}  {C : Category c₁' c₂' ℓ'} 
    ( F : Functor A C ) ( G : Functor A C ) where

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

open import Comma1 F G
open import freyd CommaCategory

open import Category.Cat

open NTrans


open Complete
open CommaObj
open CommaHom
open Limit

--  F : A → C
--  G : A → C
-- 

FIA : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I A
FIA {I} Γ = record {
  FObj = λ x → obj (FObj Γ x ) ;
  FMap = λ {a} {b} f →  arrow (FMap Γ f )  ;
  isFunctor = record {
             identity = identity
             ; distr = IsFunctor.distr (isFunctor Γ) 
             ; ≈-cong = IsFunctor.≈-cong (isFunctor Γ) 
          }} where
      identity :  {x : Obj I } → A [ arrow (FMap Γ (id1 I x)) ≈ id1 A  (obj (FObj Γ x)) ]
      identity {x} = let  open ≈-Reasoning (A) in begin
             arrow (FMap Γ (id1 I x)) 
         ≈⟨ IsFunctor.identity (isFunctor Γ)   ⟩
             id1 A  (obj (FObj Γ x))     
         ∎

NIA : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
     (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )  → NTrans I A ( K A I (obj c) )  (FIA Γ)
NIA  {I} Γ c ta = record {
        TMap = λ x → arrow (TMap ta x )
        ; isNTrans = record { commute = comm1 }
    }  where
        comm1 : {a b : Obj I} {f : Hom I a b} → 
             A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
        comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )

tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( Γ : Functor I B ) 
     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 
         ( U : Functor B C)  → NTrans I C ( K C I (FObj U lim) ) (U  ○  Γ)
tb B I Γ lim tb U = record {
               TMap  = TMap (Functor*Nat I C U tb) ; 
               isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (C) in begin
                     FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a 
                 ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
                     TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f 
                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
                 ∎
               } }

FICG : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
FICG {I} Γ = G  ○  (FIA Γ)

FICF : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
FICF {I} Γ = F  ○  (FIA Γ)

FINAT : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory ) → NTrans I C (FICF Γ) (FICG Γ)
FINAT {I} Γ = record {
       TMap = λ i → tmap i
     ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } 
   } where
        tmap :  (i : Obj I ) → Hom C (FObj (FICF Γ) i) (FObj (FICG Γ) i)
        tmap i = hom (FObj Γ i )
        commute : {a b : Obj I} → {f : Hom I a b} → C [ C [ FMap (FICG Γ) f o tmap a ] ≈ C [ tmap b o FMap (FICF Γ) f ] ]
        commute {a} {b} {f} = comm ( FMap Γ f )

revΓ : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I CommaCategory 
revΓ {I} Γ = record {
  FObj = λ x → record {
          obj = obj ( FObj Γ x )
        ; hom = TMap (FINAT Γ) x
     }
  ; FMap = λ {a} {b} f →  record {
            arrow = arrow ( FMap Γ f )
          ; comm = IsNTrans.commute ( isNTrans (FINAT Γ) )
      }
  ; isFunctor = record {
             identity = IsFunctor.identity ( isFunctor Γ )
             ; distr = IsFunctor.distr ( isFunctor Γ )
             ; ≈-cong = IsFunctor.≈-cong ( isFunctor Γ )
          }} where

NIC : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
     (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) )
NIC  {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G

LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
    → ( glimit :  ( Γ : Functor I A ) 
         → ( limita : Limit A I Γ  ) → Limit C I (G ○ Γ) ) 
    → ( Γ : Functor I CommaCategory ) 
    → Limit C I (FICG Γ) 
LimitC  {I} comp glimit Γ = glimit (FIA Γ) (isLimit comp (FIA Γ))

revLimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
    → ( glimit :  ( Γ : Functor I A ) 
         → ( limita : Limit A I Γ  ) → Limit C I (G ○ Γ) ) 
    → ( Γ : Functor I CommaCategory ) 
    → Limit C I ( G  ○ (FIA (revΓ Γ) )) 
revLimitC  {I} comp glimit Γ = glimit (FIA (revΓ Γ)) (isLimit comp (FIA (revΓ Γ )))


a0F : ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A) → Functor I A 
a0F  I a1 =  record {
  FObj = λ x →  a1
  ; FMap = λ {a} {b} f →  id1 A a1
  ; isFunctor = record {
             identity = let  open ≈-Reasoning (A) in refl-hom
             ; distr =  let  open ≈-Reasoning (A) in ( sym idL )
             ; ≈-cong = λ _ →  let  open ≈-Reasoning (A) in refl-hom
          }} where

t0F :  ( I : Category c₁ c₂ ℓ ) →  (a1 : Obj A ) 
    → NTrans I A (K A I a1 ) (a0F I a1 )
t0F  I a1  = record {
     TMap = λ i → id1 A a1 
     ; isNTrans = record { commute = λ {a b f} → commute {a} {b} {f} }
  } where
      commute : {a b : Obj I} {f : Hom I a b} → A [
        A [ FMap (a0F I a1  ) f o id1 A a1 ] ≈
        A [ id1 A a1 o FMap (K A I a1) f ] ]
      commute {a} {b} {f} =   let  open ≈-Reasoning (A) in begin
              FMap (a0F I a1 ) f o id1 A a1
         ≈⟨ idR ⟩
              FMap (a0F I a1  ) f 
         ≈⟨⟩
              id1 A a1
         ≈⟨⟩
              FMap (K A I a1) f 
         ≈↑⟨ idL ⟩
              id1 A a1 o FMap (K A I a1) f 
         ∎

hoge :  ( a : Obj A ) →   ( I : Category c₁ c₂ ℓ ) → (comp : Complete A I ) → ∀ { i : Obj I } →  
     A [ A [ TMap ( limit-u comp (a0F I a)) i o  limit (isLimit comp (a0F I a)) a (t0F I a) ]  ≈ id1 A a ]
hoge a I comp {i} = t0f=t (isLimit comp (a0F I a)) 


commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
     → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
     →  Obj CommaCategory
commaLimit {I} comp Γ glimit = record {
      obj = limit-c  comp (FIA Γ)
      ; hom = limitHom
   } where
       frev : {i : Obj I } → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
       frev {i} = TMap (t0 ( isLimit comp (FIA Γ)))  i
       tu : NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ)
       tu  = record {
              TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F frev ]
            ; isNTrans = {!!}
          }
       forward :  Hom C  (FObj G (limit-c comp (FIA Γ))) (a0 (LimitC comp glimit Γ))
       forward = limit (LimitC comp glimit Γ) (FObj G (limit-c  comp (FIA Γ))) 
            ( record { TMap = λ i →  C [ FMap G frev  o {!!} ]  ; isNTrans = {!!} } ) 
       rev :  Hom C (a0 (LimitC comp glimit Γ)) (FObj G (limit-c comp (FIA Γ)))
       rev = C [ FMap G {!!} o TMap (t0 (LimitC comp glimit Γ)) {!!} ]
       limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
       limitHom = C [  rev o limit (LimitC comp glimit Γ) (FObj F (limit-c  comp (FIA Γ))) tu ] 


commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
     → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
     → NTrans I CommaCategory (K CommaCategory I {!!}) Γ
commaNat {I} comp  Γ gilmit = record {
       TMap = λ x → {!!}
       ; isNTrans = record { commute = {!!} }
    } where


hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
    → ( glimit :  ( Γ : Functor I A ) → ( limita : Limit A I Γ ) → Limit C I (G ○ Γ) )
    → ( Γ : Functor I CommaCategory ) 
    → Limit CommaCategory I Γ 
hasLimit {I} comp glimit Γ = record {
     a0 = {!!} ;
     t0 = {!!} ;
     limit = λ a t → {!!} ;
     t0f=t = λ {a t i } →  {!!} ;
     limit-uniqueness =  λ {a} {t} f t=f →  {!!}
   }