module universal-mapping where

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

open Functor

id1 :   ∀{c₁ c₂ ℓ  : Level} (A : Category c₁ c₂ ℓ)  (a  : Obj A ) →  Hom A a a
id1 A a =  (Id {_} {_} {_} {A} a)

record IsUniversalMapping  {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) ) )
                 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
   field
       universalMapping :   {a' : Obj A} { b' : Obj B } -> { f : Hom A a' (FObj U b') } -> 
                     A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
       uniquness :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> { g :  Hom B (F a') b' } -> 
                     A [ A [ FMap U g o  η a' ]  ≈ f ] -> B [ f * ≈ g ]

record UniversalMapping  {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) ) )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    infixr 11 _*
    field
       _* :  { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) ->  Hom B (F a ) b 
       isUniversalMapping : IsUniversalMapping A B U F η _*

open NTrans
open import Category.Cat
record IsAdjunction  {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 )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
   field
       adjoint1 :   { b' : Obj B } ->
                     A [ A [ ( FMap U ( TMap ε b' ))  o ( TMap η ( FObj U b' )) ]  ≈ id1 A (FObj U b') ]
       adjoint2 :   {a' : Obj A} ->
                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ id1 B (FObj F a') ]

record Adjunction {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 )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
       isAdjunction : IsAdjunction A B U F η ε

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

open Adjunction
open UniversalMapping

Lemma1 : {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 η) 
Lemma1 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 (IsFunctor.distr ( isFunctor 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 A η) ⟩
                  (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 (IsFunctor.distr ( isFunctor 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 B ε ))  ⟩ 
                  ( 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 ) ) a (F a)   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 ) ) a (F b)  ( 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 (IsFunctor.distr ( isFunctor 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 ) a (F c)) (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 U F η um )
nat-η A B U F η um = record {
             TMap = η ; isNTrans = myIsNTrans
       } where
    F' : Functor A B
    F' = FunctorF A B U F η um
    naturality :  {a b : Obj A} {f : Hom A a b}
      → A [ A [ (FMap U (FMap F' f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
    naturality {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 { naturality = naturality }

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 U F η um ○ U) identityFunctor 
nat-ε A B U F η um = record {
             TMap = ε ; isNTrans = myIsNTrans
       } where
    F' : Functor A B
    F' = FunctorF A B U F η 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 ( IsFunctor.distr ( isFunctor 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) 
       ∎
    naturality : {a b : Obj B} {f : Hom B a b }
      →  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
    naturality {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 ) (FObj U a) b ) (lemma-nat1 a b f)) ⟩
          (_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
       ≈⟨ {!!} ⟩
          f o  ((_* um) ( id1 A (FObj U a)))
       ≈⟨⟩
          f o  (ε a)
       ∎ )
    myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
    myIsNTrans = record { naturality = naturality }