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


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
                 ∎
               } }

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 )

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 = record {
        TMap = λ x → FMap G (TMap ta x )
        ; isNTrans = record { commute = comm1 }
    }  where
          comm1 :  {a b : Obj I} {f : Hom I a b} → 
                C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] 
          comm1 {a} {b} {f} = let  open ≈-Reasoning (C) in begin
                 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
              ≈↑⟨ distr G  ⟩
                 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
              ≈⟨ fcong G  ( nat ta  ) ⟩
                 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
              ≈⟨ distr G  ⟩
                 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f  )
              ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
                 FMap G (TMap ta b) o id1 C (FObj G (obj c))
              ≈⟨⟩
                 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
              ∎


NIComma : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
     (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I CommaCategory ( K CommaCategory I c )  Γ
NIComma  {I} Γ c ta = record {
        TMap = λ x → record {
                 arrow =  TMap ta x
              ;  comm =  comm1 x
            }
        ; isNTrans = record { commute = {!!} }
    }  where
        comm1 :  ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] 
        comm1 x = let  open ≈-Reasoning (C) in begin
              FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
           ≈⟨ {!!} ⟩
              hom (FObj Γ x) o FMap F (TMap ta x) 
           ∎



commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
commaLimit {I} comp Γ = record {
      obj = limit-c  comp (FIA Γ)
      ; hom = limitHom
   } where
       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) {!!})
       limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
       limitHom = C [ FMap G ll   o C [ {!!} o FMap F ll ] ]


commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
     → (c : Obj CommaCategory )
     → ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )
     → NTrans I CommaCategory (K CommaCategory I c) Γ
commaNat {I} comp  Γ c ta = record {
       TMap = λ x → tmap x
       ; isNTrans = record { commute = {!!} }
    } where
        tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
        tmap i = record {
              arrow = A [ arrow ( TMap ta i)  o  A [  {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
              ; comm = {!!}
          }
        commute : {a b : Obj I} {f : Hom I a b} → 
              CommaCategory [ CommaCategory [ FMap Γ f o tmap a ] ≈ CommaCategory [ tmap b o FMap (K CommaCategory I c) f ] ]
        commute {a} {b} {f} = {!!}


hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
    → ( G-preserve-limit :  ( Γ : Functor I A ) 
       ( lim : Obj A ) ( ta : NTrans I A ( K A I lim ) Γ ) → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G  ) )
    → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I (commaLimit comp Γ) ) Γ ) 
    → Limit CommaCategory I Γ (commaLimit comp Γ ) ( commaNat comp  Γ (commaLimit comp Γ) ta ) 
hasLimit {I} comp gpresrve Γ ta  = record {
     limit = λ a t → {!!} ;
     t0f=t = λ {a t i } →  {!!} ;
     limit-uniqueness =  λ {a} {t} f t=f →  {!!}
   }