module universal-mapping where

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

open Functor

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 ]
       unique-universalMapping :   (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' )) ]  ≈ Id {_} {_} {_} {A} (FObj U b') ]
       adjoint2 :   {a' : Obj A} ->
                     B [ B [ ( TMap ε ( FObj F a' ))  o ( FMap F ( TMap η a' )) ]  ≈ Id {_} {_} {_} {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 η ε

open Adjunction
open UniversalMapping

Solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                 ( U : Functor B A )
                 ( F : Functor A B )
                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) ->
     { a : Obj A} { b : Obj B} -> ( f : Hom A a (FObj U b) ) ->  Hom B (FObj F a ) b 
Solution  A B U F ε {a} {b} f = B [ TMap ε b o FMap F f ]

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 A B U F ε ;
         isUniversalMapping = record {
                    universalMapping  = universalMapping
              }
      } where
         universalMapping :   (a' : Obj A) ( b' : Obj B ) -> { f : Hom A a' (FObj U b') } -> 
                     A [ A [ FMap U ( Solution A B U F ε f  ) o TMap η a' ]  ≈ f ]
         universalMapping a b {f} = 
           let open ≈-Reasoning (A) in
              begin 
                  FMap U ( Solution A B U F ε 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
              ∎


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-id-1 :  {a : Obj A} ->  A [ A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ]  ≈ (A [ (η a) o (Id {_} {_} {_} {A} a) ]) ]
    lemma-id-1 {a} = let open ≈-Reasoning (A) in
       begin
            A [ FMap U (Id {_} {_} {_} {B} (F a))  o  η a ] 
       ≈⟨ ( car ( IsFunctor.identity ( isFunctor U )))  ⟩
            A [ (Id {_} {_} {_} {A} (FObj U ( F a )) ) o  η a ] 
       ≈⟨ idL  ⟩
           η a
       ≈⟨ sym idR  ⟩
           (A [ (η a) o (Id {_} {_} {_} {A} a) ]) 
       ∎
    lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (Id {_} {_} {_} {A} a)] )) ≈ (Id {_} {_} {_} {B} (F a)) ]
    lemma-id {a} =   ( IsUniversalMapping.unique-universalMapping ( isUniversalMapping um ) ) 
              a (F a)  ((A [ (η a) o (Id {_} {_} {_} {A} a)] )) ((Id {_} {_} {_} {B} (F a))) lemma-id-1
    myIsFunctor : IsFunctor A B F myFMap
    myIsFunctor =
      record { ≈-cong   = {!!}
             ; identity = lemma-id
             ; distr    = {!!}
             }