-- Pullback from product and equalizer
--
--
--                        Shinji KONO <kono@ie.u-ryukyu.ac.jp>
----

open import Category -- https://github.com/konn/category-agda
open import Level
module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where

open import HomReasoning
open import cat-utility

-- 
-- Pullback from equalizer and product
--         f
--     a -------> c
--     ^          ^                 
--  π1 |          |g
--     |          |
--    ab -------> b
--     ^   π2
--     |
--     | e = equalizer (f π1) (g π1)  
--     |
--     d <------------------ d'
--         k (π1' × π2' )

open Equalizer
open Product
open Pullback

pullback-from :  (a b c ab d : Obj A) 
      ( f : Hom A a c )    ( g : Hom A b c )
      ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) ( e : Hom A d ab )
      ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g ) 
      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g 
          ( A [  π1 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
          ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] ) 
pullback-from  a b c ab d f g π1 π2 e eqa prod =  record {
              commute = commute1 ;
              p = p1 ; 
              π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11  {d} {π1'} {π2'} {eq} ; 
              π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ; 
              uniqueness = uniqueness1
      } where 
      commute1 :  A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
      commute1 = let open ≈-Reasoning (A) in
             begin
                    f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) 
             ≈⟨ assoc ⟩
                    ( f o  π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) 
             ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
                    ( g o  π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) 
             ≈↑⟨ assoc ⟩
                    g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) 
             ∎
      lemma1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → 
                      A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
      lemma1  {d'} { π1' } { π2' } eq  = let open ≈-Reasoning (A) in 
             begin
                    ( f o π1 ) o (prod × π1') π2'
             ≈↑⟨ assoc ⟩
                     f o ( π1  o (prod × π1') π2' )
             ≈⟨ cdr (π1fxg=f prod)  ⟩
                     f o  π1'
             ≈⟨ eq ⟩
                     g o  π2'
             ≈↑⟨ cdr (π2fxg=g prod)  ⟩
                     g o ( π2  o (prod × π1') π2'  )
             ≈⟨ assoc ⟩
                    ( g o π2 ) o (prod × π1') π2'
             ∎
      p1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d
      p1 {d'} { π1' } { π2' } eq  = 
         let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) ( lemma1 eq )
      π1p=π11 :   {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 
            A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
      π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
             begin
                     ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
             ≈⟨⟩
                     ( π1 o e) o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
             ≈↑⟨ assoc ⟩
                      π1 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
             ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
                      π1 o  (_×_ prod  π1'  π2' ) 
             ≈⟨ π1fxg=f prod ⟩
                     π1'
             ∎
      π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 
            A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
      π2p=π21  {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
             begin
                     ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq
             ≈⟨⟩
                     ( π2 o e) o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
             ≈↑⟨ assoc ⟩
                      π2 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
             ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
                      π2 o  (_×_ prod  π1'  π2' ) 
             ≈⟨ π2fxg=g prod ⟩
                     π2'
             ∎
      uniqueness1 :  {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
        {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} →
        {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} →
        A [ p1 eq ≈ p' ]
      uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in
             begin
                 p1 eq
             ≈⟨⟩
                 k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq)
             ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin
                 e o p'
             ≈⟨⟩
                  equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'
             ≈↑⟨ Product.uniqueness prod ⟩
                (prod × (  π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
             ≈⟨ ×-cong prod (assoc) (assoc) ⟩
                 (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
                         (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) 
             ≈⟨ ×-cong prod eq1 eq2 ⟩
                ((prod × π1') π2')
             ∎ ) ⟩
                 p'
             ∎

------
--
-- Limit
--
-----

-- Constancy Functor

K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A
K I a = record {
      FObj = λ i → a ;
      FMap = λ f → id1 A a ;
        isFunctor = let  open ≈-Reasoning (A) in record {
               ≈-cong   = λ f=g → refl-hom
             ; identity = refl-hom
             ; distr    = sym idL
        }
  }

open NTrans

record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 
     ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
  field
     limit :  ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
     t0f=t :  { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } →
         A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
     limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ∀ ( i : Obj I ) →
         A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] → A [ limit a t ≈ f ]

--------------------------------
--
-- If we have two limits on c and c', there are isomorphic pair h, h'

open Limit

iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
      → Hom A a0 a0'
iso-l  I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0

iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
      → Hom A a0' a0
iso-r  I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'


iso-lr :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )  → ∀{ i : Obj I } →
  A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim'  ]  ≈ id1 A a0' ]
iso-lr  I Γ a0 a0' t0 t0' lim lim' {i} =  let open ≈-Reasoning (A) in begin
           limit lim' a0 t0 o limit lim a0' t0'
      ≈↑⟨ limit-uniqueness lim' i ( begin
          TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
      ≈⟨ assoc  ⟩
          ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0' 
      ≈⟨ car ( t0f=t lim' ) ⟩
          TMap t0 i o limit lim a0' t0' 
      ≈⟨ t0f=t lim ⟩
          TMap t0' i 
      ∎ ) ⟩
           limit lim' a0' t0'
      ≈⟨ limit-uniqueness lim' i idR ⟩
           id a0'
      ∎


open import CatExponetial 

open Functor

--------------------------------
--
-- Contancy Functor

KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) →  Functor A ( A ^ I )
KI { c₁'} {c₂'} {ℓ'} I = record {
      FObj = λ a → K I a ;
      FMap = λ f → record { --  NTrans I A (K I a)  (K I b)
            TMap = λ a → f ;
            isNTrans = record { 
                 commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
            }
        }  ; 
        isFunctor = let  open ≈-Reasoning (A) in record {
               ≈-cong   = λ f=g {x} → f=g
             ; identity = refl-hom
             ; distr    = refl-hom
        }
  } where
     commute1 :  {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
        A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ]
     commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin 
            FMap (K I b') f₁ o f 
        ≈⟨ idL ⟩
           f
        ≈↑⟨ idR ⟩
            f o FMap (K I a') f₁ 
        ∎


open import Function

limit2adjoint : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
     ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) 
     ( lim : Limit I Γ a0 t0 ) →  coUniversalMapping A ( A ^ I ) (KI I) ({!!}) ({!!})
limit2adjoint = {!!}