module universal-mapping where

-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>

open import Category -- https://github.com/konn/category-agda
open import Level
open import HomReasoning
open import cat-utility
open import Category.Cat

open Functor
open NTrans

--
--   Adjunction yields solution of universal mapping 
--
--

open Adjunction
open UniversalMapping

Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                 { U : Functor B A }
                 { F : Functor A B }
                 { η : NTrans A A identityFunctor ( U ○  F ) }
                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
      Adjunction A B U F η ε  → UniversalMapping A B U (FObj F) (TMap η) 
Adj2UM A B {U} {F} {η} {ε} adj = record {
         _* = solution  ;
         isUniversalMapping = record {
                    universalMapping  = universalMapping;
                    uniquness = uniqness
              }
      } where
         solution :  { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) →  Hom B (FObj F a ) b 
         solution  {_} {b} f = B [ TMap ε b o FMap F f ]
         universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
                     A [ A [ FMap U ( solution f) o TMap η a' ]  ≈ f ]
         universalMapping {a} {b} {f} = 
           let open ≈-Reasoning (A) in
              begin 
                  FMap U ( solution  f) o TMap η a 
              ≈⟨⟩
                  FMap U (  B [ TMap ε b o FMap F f ] ) o TMap η a 
              ≈⟨ car (distr U ) ⟩
                 ( (FMap U (TMap ε b))  o (FMap U ( FMap F f )) ) o TMap η a 
              ≈⟨ sym assoc ⟩
                  (FMap U (TMap ε b))  o ((FMap U ( FMap F f ))  o TMap η a )
              ≈⟨ cdr (nat η) ⟩
                  (FMap U (TMap ε b))  o ((TMap η (FObj U b )) o f )
              ≈⟨ assoc ⟩
                  ((FMap U (TMap ε b))  o (TMap η (FObj U b)))  o f 
              ≈⟨ car ( IsAdjunction.adjoint1 ( isAdjunction adj))  ⟩
                  id (FObj U b) o f
              ≈⟨  idL  ⟩
                  f
              ∎
         lemma1 : (a : Obj A) ( b : Obj B ) ( f : Hom A a (FObj U b) ) → ( g :  Hom B (FObj F a) b) →
                A [ A [ FMap U g o  TMap η a ]  ≈ f ] →
                B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ] 
         lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
         uniqness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (FObj F a') b'} → 
                     A [ A [ FMap U g o  TMap η a' ]  ≈ f ] → B [ solution f  ≈ g ]
         uniqness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
              begin 
                  solution f 
              ≈⟨⟩
                  TMap ε b o FMap F f
              ≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩ 
                  TMap ε b o FMap F ( A [ FMap U g o  TMap η a ] )
              ≈⟨ cdr (distr F )  ⟩ 
                  TMap ε b o ( FMap F ( FMap U g)  o FMap F ( TMap η a ) )
              ≈⟨ assoc  ⟩ 
                  ( TMap ε b o  FMap F ( FMap U g) ) o FMap F ( TMap η a ) 
              ≈⟨ sym ( car ( nat ε ))  ⟩ 
                  ( g o TMap ε ( FObj F a) )  o FMap F ( TMap η a ) 
              ≈⟨ sym assoc ⟩ 
                  g o ( TMap ε ( FObj F a)   o FMap F ( TMap η a ) )
              ≈⟨ cdr ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩ 
                  g o id (FObj F a)
              ≈⟨ idR ⟩ 
                  g
              ∎

--
--
--  Universal mapping yields Adjunction
--
--


--
-- F is an functor
--

FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                 { U : Functor B A }
                 { F : Obj A → Obj B }
                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
       UniversalMapping A B U F η   → Functor A B
FunctorF A B {U} {F} {η} um = record {
              FObj = F;
              FMap = myFMap ;
              isFunctor = myIsFunctor
       } where
    myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b)
    myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ]) 
    lemma-id1 :  {a : Obj A} →  A [ A [ FMap U (id1 B (F a))  o  η a ]  ≈ (A [ (η a) o (id1 A a) ]) ]
    lemma-id1 {a} = let open ≈-Reasoning (A) in
       begin
           FMap U (id1 B (F a))  o  η a 
       ≈⟨ ( car ( IsFunctor.identity ( isFunctor U )))  ⟩
           id (FObj U ( F a )) o  η a 
       ≈⟨ idL  ⟩
           η a
       ≈⟨ sym idR  ⟩
           η a o id a
       ∎
    lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ]
    lemma-id {a} =   ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) lemma-id1
    lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → 
                A [ A [ FMap U ((_* um) (A [ η b  o  g ]) ) o  η a ] ≈  A [ η b  o  f ] ]
    lemma-cong2 a b f g eq =  let open ≈-Reasoning (A) in
       begin
          ( FMap U ((_* um) (A [ η b  o  g ]) )) o  η a 
       ≈⟨  ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
          η b  o  g 
       ≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom)  ) ⟩
          η b  o  f 
       ∎
    lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b  o  f ] ) ≈  (_* um) (A [ η b  o  g ]) ]
    lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( isUniversalMapping um ) ) ( lemma-cong2 a b f g eq )
    lemma-cong :  {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ]
    lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq
    lemma-distr2 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
            A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ])  o  η a ] ≈ (A [ η c o A [ g o f ] ]) ]
    lemma-distr2 a b c f g = let open ≈-Reasoning (A) in
       begin
           ( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] ) )  o  η a 
       ≈⟨ car (distr U )  ⟩
           (( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b  o f ])))) )   o  η a 
       ≈⟨ sym assoc ⟩
           ( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b  o f ]))))   o  η a )
       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
           ( FMap U ((_* um) (A [ η c o g ])) o ( η b  o f) )
       ≈⟨ assoc ⟩
           ( FMap U ((_* um) (A [ η c o g ])) o  η b)  o f
       ≈⟨ car ( IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
           (  η c o g )  o f
       ≈⟨ sym assoc  ⟩
            η c o ( g o f )
       ∎
    lemma-distr1 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) → 
            B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )]
    lemma-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( isUniversalMapping um )) (lemma-distr2 a b c f g )
    lemma-distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )]
    lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g 
    myIsFunctor : IsFunctor A B F myFMap
    myIsFunctor =
      record { ≈-cong   = lemma-cong
             ; identity = lemma-id
             ; distr    = lemma-distr
             }

--
-- naturality of η
--
nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                 { U : Functor B A }
                 { F : Obj A → Obj B }
                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
       (um : UniversalMapping A B U F η )  → 
           NTrans  A A identityFunctor ( U ○ FunctorF A B um )
nat-η A B {U} {F} {η} um = record {
             TMap = η ; isNTrans = myIsNTrans
       } where
    F' : Functor A B
    F' = FunctorF A B um
    commute :  {a b : Obj A} {f : Hom A a b}
      → A [ A [ (FMap U (FMap F' f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
    commute {a} {b} {f} =   let open ≈-Reasoning (A) in
       begin
            (FMap U (FMap F' f))  o  ( η a ) 
       ≈⟨⟩
            (FMap U ((_* um)  (A [  η b  o f ])))   o  ( η a ) 
       ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
            (η b ) o f 
       ∎
    myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
    myIsNTrans = record { commute = commute }

nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                 { U : Functor B A }
                 { F : Obj A → Obj B }
                 { η : (a : Obj A) → Hom A a ( FObj U (F a) ) } →
       (um : UniversalMapping A B U F η )  → 
           NTrans B B ( FunctorF A B um ○ U) identityFunctor 
nat-ε A B {U} {F} {η} um = record {
             TMap = ε ; isNTrans = myIsNTrans
       } where
    F' : Functor A B
    F' = FunctorF A B um
    ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b
    ε b = (_* um) ( id1 A (FObj U b))
    lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) → 
             A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] )  o η (FObj U a) ]
                 ≈ A [ FMap U f o id1 A (FObj U a) ] ]
    lemma-nat1 a b f = let open ≈-Reasoning (A) in
       begin 
          FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] )  o η (FObj U a) 
       ≈⟨ car ( distr U  ) ⟩
          ( FMap U  ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) )  o η (FObj U a) 
       ≈⟨ sym assoc  ⟩
           FMap U  ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f )))  o η (FObj U a) 
       ≈⟨ cdr ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) )  ⟩
           FMap U  ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f )
       ≈⟨ assoc  ⟩
           (FMap U  ((um *) (id1 A (FObj U b))) o  η (FObj U b)) o FMap U f 
       ≈⟨ car ((IsUniversalMapping.universalMapping ( isUniversalMapping um )) ) ⟩
           id1 A (FObj U b) o FMap U f 
       ≈⟨ idL ⟩
            FMap U f 
       ≈⟨ sym idR ⟩
          FMap U f o id (FObj U a) 
       ∎
    lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
                                                        ≈ A [ FMap U f o id1 A (FObj U a) ] ]
    lemma-nat2 a b f = let open ≈-Reasoning (A) in
       begin
          FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ])  o η (FObj U a) 
       ≈⟨ car ( distr U  ) ⟩
          (FMap U f o FMap U ((um *) (id1 A (FObj U a ))))  o η (FObj U a) 
       ≈⟨ sym assoc  ⟩
          FMap U f o ( FMap U ((um *) (id1 A (FObj U a )))  o η (FObj U a)  )
       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
          FMap U f o id (FObj U a )
       ∎
    commute : {a b : Obj B} {f : Hom B a b }
      →  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
    commute {a} {b} {f} = let open ≈-Reasoning (B) in
       sym ( begin
          ε b o (FMap F' (FMap U f))
       ≈⟨⟩
          ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
       ≈⟨⟩
          ((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
       ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-nat1 a b f))) ⟩
          (_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
       ≈⟨ (IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-nat2 a b f)) ⟩
          f o  ((_* um) ( id1 A (FObj U a)))
       ≈⟨⟩
          f o  (ε a)
       ∎ )
    myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
    myIsNTrans = record { commute = commute }

------
--
--   Adjunction Construction from Universal Mapping
--
-----

UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                 ( U : Functor B A )
                 ( F' : Obj A → Obj B )
                 ( η' : (a : Obj A) → Hom A a ( FObj U (F' a) ) ) →
       (um : UniversalMapping A B U F' η' )  → 
              Adjunction A B U (FunctorF A B um) (nat-η A B um) (nat-ε A B  um)
UMAdjunction A B U F' η' um = record {
           isAdjunction = record {
               adjoint1 = adjoint1 ; 
               adjoint2 = adjoint2
           } 
       } where
          F : Functor A B
          F = FunctorF A B um
          η : NTrans A A identityFunctor ( U ○  F ) 
          η = nat-η A B um
          ε : NTrans B B  ( F ○  U ) identityFunctor 
          ε = nat-ε A B um
          adjoint1 :   { b : Obj B } →
                     A [ A [ ( FMap U ( TMap ε b ))  o ( TMap η ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
          adjoint1 {b} = let open ≈-Reasoning (A) in
             begin
               FMap U ( TMap ε b )  o  TMap η ( FObj U b )
             ≈⟨⟩
               FMap U ((_* um) ( id1 A (FObj U b)))  o  η' ( FObj U b )
             ≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um )  ⟩
               id (FObj U b) 
             ∎
          lemma-adj1 : (a : Obj A) → 
             A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ] 
               ≈ (η' a) ]
          lemma-adj1 a =  let open ≈-Reasoning (A) in
             begin
               FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a 
             ≈⟨ car (distr U)  ⟩
               (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a 
             ≈⟨ sym assoc ⟩
               FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a )
             ≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
               FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) )
             ≈⟨ assoc ⟩
               (FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a )
             ≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
                id (FObj U ( FObj F a)) o ( η' a )
             ≈⟨ idL ⟩
               η' a
             ∎
          lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈  η' a ]
          lemma-adj2 a = let open ≈-Reasoning (A) in
             begin
               FMap U (id1 B (FObj F a)) o η' a 
             ≈⟨  car ( IsFunctor.identity ( isFunctor U))  ⟩
               id (FObj U (FObj F a)) o η' a 
             ≈⟨ idL ⟩
               η' a 
             ∎
          adjoint2 :   {a : Obj A} →
                     B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]
          adjoint2 {a} = let open ≈-Reasoning (B) in
             begin
                TMap ε ( FObj F a )  o  FMap F ( TMap η a )
             ≈⟨⟩
                ((_* um) ( id1 A (FObj U ( FObj F a ))))  o  (_* um)  (A [  η' (FObj U ( FObj F a ))   o ( η' a ) ])
             ≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj1 a))) ⟩
                (_* um)( η' a )
             ≈⟨  IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj2 a) ⟩
                id1 B (FObj F a)
             ∎


--  done!