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
open IsLimit

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

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 Γ)

open LimitPreserve

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

frev :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory ) (i : Obj I ) → Hom A (limit-c comp (FIA Γ)) (obj (FObj Γ i))
frev comp Γ i = TMap (t0 ( climit comp (FIA Γ)))  i

tu :  { I : Category c₁ c₂ ℓ } →  ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
    →   NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (FICG Γ)
tu {I} comp Γ = record {
      TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F (frev comp Γ i) ]
    ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
  } where
        commute : {a b : Obj I} {f : Hom I a b}   →
              C [ C [ FMap (FICG Γ) f o C [ hom (FObj Γ a) o FMap F (frev comp Γ a) ] ] 
            ≈ C [ C [ hom (FObj Γ b) o FMap F (frev comp Γ b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
        commute  {a} {b} {f} =  let  open ≈-Reasoning (C) in begin
             FMap (FICG Γ) f o ( hom (FObj Γ a) o FMap F (frev comp Γ a) )
         ≈⟨⟩
             FMap G (arrow (FMap Γ f ) ) o ( hom (FObj Γ a) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ))
         ≈⟨ assoc ⟩
             (FMap G (arrow (FMap Γ f ) ) o  hom (FObj Γ a)) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a )
         ≈⟨ car ( comm (FMap Γ f))  ⟩
              (hom (FObj Γ b) o FMap F (arrow (FMap Γ f)) ) o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a )
         ≈↑⟨ assoc ⟩
              hom (FObj Γ b) o ( FMap F (arrow (FMap Γ f))  o FMap F ( TMap (t0 ( climit comp (FIA Γ)))  a ) )
         ≈↑⟨  cdr (distr F)  ⟩
              hom (FObj Γ b) o ( FMap F (A [ arrow (FMap Γ f)  o TMap (t0 ( climit comp (FIA Γ)))  a ] ) )
         ≈⟨⟩
              hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ)  f  o TMap (t0 ( climit comp (FIA Γ)))  a ] ) )
         ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ)))  ))) ⟩
              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] ))
         ≈⟨⟩
              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] ))
         ≈⟨ cdr ( distr F ) ⟩
              hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o FMap F (id1 A (limit-c comp (FIA Γ))))
         ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩
              hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ))))
         ≈⟨ assoc ⟩
             ( hom (FObj Γ b) o FMap F (frev comp Γ b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f
         ∎
limitHom :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory )
    → ( glimit :  LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )

commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
    → ( glimit :  LimitPreserve A I C G )
    →  Obj CommaCategory
commaLimit {I} comp Γ glimit = record {
      obj = limit-c  comp (FIA Γ)
      ; hom = limitHom comp Γ glimit
   } 


commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
     → ( glimit :   LimitPreserve A I C G )
     → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit))  Γ
commaNat {I} comp  Γ glimit = record {
       TMap = λ x → record {
              arrow =  TMap ( limit-u comp (FIA Γ ) ) x 
            ; comm  = comm1 x
          } 
       ; isNTrans = record { commute = comm2 }
    } where
       comm1 : (x : Obj I )  →
              C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] 
            ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] 
       comm1 x =  let  open ≈-Reasoning (C) in begin
              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x)
         ≈⟨⟩
              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) 
         ≈⟨⟩
              FMap G (TMap (limit-u comp (FIA Γ)) x) o limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
         ≈⟨⟩
              TMap (t0 ( LimitC comp Γ glimit )) x  o limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
         ≈⟨ t0f=t ( isLimit (  LimitC comp Γ glimit ) ) ⟩
              TMap (tu comp Γ) x 
         ≈⟨⟩
              hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x)
         ∎
       comm2 : {a b : Obj I} {f : Hom I a b} →
          CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ]
          ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ]
       comm2 {a} {b} {f} =  let  open ≈-Reasoning (CommaCategory) in begin
             FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } 
         ≈⟨ {!!} ⟩
             record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f 
         ∎


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