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 ]

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

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) ?  ?
Lemma1 = ?