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

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 )


open LimitPreserve

LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
    → ( Γ : Functor I CommaCategory ) 
    → ( glimit :  LimitPreserve A I  C G )
    → Limit C I (G  ○  (FIA Γ)) 
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 Γ)))) (G  ○  (FIA Γ))
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 (G  ○  (FIA Γ)) 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 (G  ○  (FIA Γ)) 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 (A) in begin
              FMap (FIA Γ) f  o TMap (limit-u comp (FIA Γ)) a 
         ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ)))   ⟩
              TMap (limit-u comp (FIA Γ)) b  o FMap (K A I (limit-c comp (FIA Γ))) f 
         ∎

comma-a0 :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
comma-a0  {I} comp Γ glimit a t = record {
       arrow  = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
     ; comm = comm1
   } where
      comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ]
        ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ]
      comm1 =  let  open ≈-Reasoning (C) in begin
            FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a 
         ≈⟨ {!!} ⟩
            limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )  o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
         ≈⟨⟩
            hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))
         ∎

comma-t0f=t :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) (i : Obj I )
     →   CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ]
comma-t0f=t  {I} comp Γ glimit a t i = let  open ≈-Reasoning (A) in begin
             TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
         ≈⟨ t0f=t (isLimit ( climit comp (FIA Γ) ) )  ⟩
             TMap (NIA  {I} Γ a t ) i
         ∎


comma-uniqueness :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) 
     →  ( f :  Hom CommaCategory a  (commaLimit comp Γ glimit)) 
     →   ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat {  I} comp Γ glimit ) i o  f ]  ≈ TMap t i ] )
     → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ]
comma-uniqueness  {I} comp Γ glimit a t f t=f    = let  open ≈-Reasoning (A) in begin
             limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
         ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f)  t=f ⟩
             arrow 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 → comma-a0 comp Γ glimit a t ;
             t0f=t = λ {a t i } →  comma-t0f=t  comp Γ glimit a t i ;
             limit-uniqueness =  λ {a} {t} f t=f →  comma-uniqueness  {I} comp Γ glimit a t f t=f
     }
   }