# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1510403698 -32400
# Node ID a5f2ca67e7c59c7c6b6fe88336523bb86cd38382
# Parent  d0bc017c6b61c502d0fa7e350bbc5a2f43e59cc4
fix monad/adjunction definition
couniversal to limit does not work

diff -r d0bc017c6b61 -r a5f2ca67e7c5 adj-monad.agda
--- a/adj-monad.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/adj-monad.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -20,7 +20,6 @@
 --
 ----
 
-open Adjunction
 open NTrans
 open Functor
 
@@ -35,18 +34,25 @@
          lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}
 
 Adj2Monad : {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 η ε  → Monad A (U ○  F) η (UεF A B U F ε)
-Adj2Monad A B {U} {F} {η} {ε} adj = record {
+       → Adjunction A B → Monad A 
+Adj2Monad A B adj = record {
+         T = T ;
+         η = η ;
+         μ = μ ;
          isMonad = record {
                     assoc = assoc1;
                     unity1 = unity1;
                     unity2 = unity2
               }
       }  where
+           U : Functor B A 
+           U = Adjunction.U adj
+           F : Functor A B 
+           F = Adjunction.F adj
+           η : NTrans A A identityFunctor ( U ○  F ) 
+           η = Adjunction.η adj
+           ε : NTrans B B  ( F ○  U ) identityFunctor 
+           ε = Adjunction.ε adj
            T : Functor A A
            T = U  ○ F
            μ : NTrans A A ( T ○ T ) T
@@ -75,7 +81,7 @@
                TMap μ a o TMap η ( FObj T a )
              ≈⟨⟩
                (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
-             ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
+             ≈⟨ IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj ) ⟩
                id (FObj U ( FObj F a ))
              ≈⟨⟩
                id (FObj T a)
@@ -88,7 +94,7 @@
                 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
              ≈⟨ sym (distr U ) ⟩
                 FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
-             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
+             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
                 FMap U ( id1 B (FObj F a) )
              ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
                 id (FObj T a)
diff -r d0bc017c6b61 -r a5f2ca67e7c5 cat-utility.agda
--- a/cat-utility.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/cat-utility.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -26,12 +26,12 @@
                              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
+               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
                isUniversalMapping : IsUniversalMapping A B U F η _*
 
@@ -48,12 +48,12 @@
                              B [ B [ ε b o FMap F g ]  ≈ f ] → A [ f *' ≈ g ]
 
         record coUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
-                         ( F : Functor A B )
-                         ( U : Obj B → Obj A )
-                         ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b )
                          : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
             infixr 11 _*'
             field
+               F : Functor A B 
+               U : Obj B → Obj A 
+               ε : (b : Obj B) → Hom B ( FObj F (U b) ) b 
                _*' :  { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) →  Hom A a (U b )
                iscoUniversalMapping : coIsUniversalMapping A B F U ε _*'
 
@@ -72,12 +72,12 @@
                              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
+               U : Functor B A 
+               F : Functor A B 
+               η : NTrans A A identityFunctor ( U ○  F ) 
+               ε : NTrans B B  ( F ○  U ) identityFunctor 
                isAdjunction : IsAdjunction A B U F η ε
             U-functor =  U
             F-functor =  F
@@ -95,9 +95,12 @@
               unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
               unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
 
-        record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
+        record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
           field
+            T : Functor A A
+            η : NTrans A A identityFunctor T
+            μ : NTrans A A (T ○ T) T
             isMonad : IsMonad A T η μ
              -- g ○ f = μ(c) T(g) f
           join : { a b : Obj A } → { c : Obj A } →
@@ -143,20 +146,17 @@
         --      nat-ε
         --      nat-η     -- same as η but has different types
 
-        record MResolution {c₁ c₂ ℓ  c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' )
-              ( T : Functor A A )
-              -- { η : NTrans A A identityFunctor T }
-              -- { μ : NTrans A A (T ○ T) T }
-              -- { M : Monad A T  η μ }
-              ( UR : Functor B A ) ( FR : Functor A B )
-              { ηR : NTrans A A identityFunctor  ( UR ○ FR ) }
-              { εR : NTrans B B ( FR ○ UR ) identityFunctor }
-              { μR : NTrans A A ( (UR ○ FR)  ○ ( UR ○ FR )) ( UR ○ FR  ) }
-              ( Adj : Adjunction A B UR FR ηR εR  )
-                        : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-                   field
-                      T=UF  :  T ≃  (UR ○ FR)
-                      μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
+        record MResolution {c₁ c₂ ℓ  c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) ( M : Monad A )
+           : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+             field
+              UR : Functor B A
+              FR : Functor A B 
+              ηR : NTrans A A identityFunctor  ( UR ○ FR ) 
+              εR : NTrans B B ( FR ○ UR ) identityFunctor 
+              μR : NTrans A A ( (UR ○ FR)  ○ ( UR ○ FR )) ( UR ○ FR  ) 
+              Adj : IsAdjunction A B UR FR ηR εR  
+              T=UF  :  Monad.T M ≃  (UR ○ FR)
+              μ=UεF : {x : Obj A } → A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
                       -- ηR=η  : {x : Obj A } → A [ TMap ηR x  ≈  TMap η x ] -- We need T → UR FR conversion
                       -- μR=μ  : {x : Obj A } → A [ TMap μR x  ≈  TMap μ x ]
 
@@ -381,8 +381,13 @@
 
 -- initial object
 
-        record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+        record IsInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
           field
              initial :  ∀( a : Obj A ) →  Hom A i a
              uniqueness  : { a : Obj A } →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
+        record InitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
+          field
+             initialObject :  Obj A 
+             isInitialObject :  IsInitialObject A initialObject
+
diff -r d0bc017c6b61 -r a5f2ca67e7c5 comparison-em.agda
--- a/comparison-em.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/comparison-em.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -19,14 +19,13 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M' : Monad A T η μ }
+                 { M' : IsMonad A T η μ }
       {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U^K : Functor B A } { F^K : Functor A B }
       { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) }
       { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor } 
       { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
-      ( Adj^K : Adjunction A B U^K F^K η^K ε^K )
-      ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K )
+      ( Adj^K : IsAdjunction A B U^K F^K η^K ε^K )
   where
 
 open import adj-monad
@@ -36,8 +35,8 @@
 μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) 
 μ^K'  = UεF A B U^K F^K ε^K 
 
-M : Monad A (U^K ○ F^K ) η^K μ^K' 
-M =  Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K
+M : IsMonad A (U^K ○ F^K ) η^K μ^K' 
+M = Monad.isMonad ( Adj2Monad A B ( record { U = U^K; F = F^K ; η = η^K ; ε = ε^K ; isAdjunction =  Adj^K } ) )
 
 open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K' } { M } 
 
@@ -55,7 +54,7 @@
       identity1 b =  let open ≈-Reasoning (A) in
            begin
                 (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b)
-           ≈⟨ IsAdjunction.adjoint1 (isAdjunction Adj^K) ⟩
+           ≈⟨ IsAdjunction.adjoint1 Adj^K ⟩
                 id1 A (FObj U^K b)
            ∎
 
diff -r d0bc017c6b61 -r a5f2ca67e7c5 comparison-functor.agda
--- a/comparison-functor.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/comparison-functor.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -19,14 +19,13 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M' : Monad A T η μ }
+                 { M' : IsMonad A T η μ }
       {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U_K : Functor B A } { F_K : Functor A B }
       { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
       { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 
       { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
-      ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK )
+      ( AdjK : IsAdjunction A B U_K F_K η_K ε_K )
    where
 
 open import adj-monad
@@ -36,8 +35,8 @@
 μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) 
 μ_K  = UεF A B U_K F_K ε_K 
 
-M : Monad A (U_K ○ F_K ) η_K μ_K 
-M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
+M : IsMonad A (U_K ○ F_K ) η_K μ_K 
+M = Monad.isMonad ( Adj2Monad A B ( record { U = U_K; F = F_K ; η = η_K ; ε = ε_K ; isAdjunction =  AdjK } ) )
 
 open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 
 
@@ -68,7 +67,7 @@
                TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a}))
            ≈⟨⟩
               TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
-           ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
+           ≈⟨ IsAdjunction.adjoint2 AdjK ⟩
               id1 B (FObj F_K a)
            ∎
          ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
@@ -144,7 +143,7 @@
              TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b)  o FMap F_K f )
            ≈⟨ assoc  ⟩
              (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b))  o FMap F_K f 
-           ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩
+           ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩
              id1 B (FObj F_K b)  o FMap F_K f 
            ≈⟨ idL  ⟩
              FMap F_K f 
@@ -170,7 +169,7 @@
                  FMap K_T  (record { KMap = (TMap η_K b) })
            ≈⟨⟩  
                  TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)
-           ≈⟨  IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩  
+           ≈⟨  IsAdjunction.adjoint2 AdjK ⟩  
                  id1 B (FObj F_K b)
            ∎
 
@@ -185,7 +184,7 @@
                 TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g )
            ≈⟨ assoc ⟩
                 (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g 
-           ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩  
+           ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩  
                  id1 B (FObj F_K (FObj T_K c)) o FMap F_K g 
            ≈⟨ idL ⟩
                 FMap F_K g 
diff -r d0bc017c6b61 -r a5f2ca67e7c5 em-category.agda
--- a/em-category.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/em-category.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -24,7 +24,7 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } where
+                 { M : IsMonad A T η μ } where
 
 --
 --  Hom in Eilenberg-Moore Category
@@ -104,7 +104,7 @@
 -- cannot use as identityL = EMidL
 --
 EMidL : {C D : EMObj} → {f : EMHom C D} → (EM-id  ∙ f) ≗ f
-EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D} 
+EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj C} 
 EMidR : {C D : EMObj} → {f : EMHom C D} → (f ∙ EM-id)  ≗ f
 EMidR {C} {_} {_} = let open ≈-Reasoning (A) in  idR {obj C}
 EMo-resp :  {a b c : EMObj} → {f g : EMHom a b } → {h i : EMHom  b c } → 
@@ -157,12 +157,11 @@
         }
      } where open ≈-Reasoning (A) 
 
-open Monad
 Lemma-EM4 : (x : Obj A ) → A [ A [ TMap μ x  o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
 Lemma-EM4 x = let  open ≈-Reasoning (A) in
     begin
        TMap μ x  o TMap η (FObj T x) 
-    ≈⟨ IsMonad.unity1 (isMonad M) ⟩
+    ≈⟨ IsMonad.unity1 M ⟩
        id1 A (FObj T x)
     ∎
 
@@ -170,7 +169,7 @@
 Lemma-EM5 x =  let  open ≈-Reasoning (A) in
     begin
        ( TMap μ x)  o TMap μ (FObj T x) 
-    ≈⟨ IsMonad.assoc (isMonad M) ⟩
+    ≈⟨ IsMonad.assoc M ⟩
        ( TMap μ x) o FMap T ( TMap μ x)
     ∎
 
@@ -312,8 +311,12 @@
               TMap μ x
           ∎ )
 
-Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
+Adj^T : Adjunction A Eilenberg-MooreCategory 
 Adj^T = record {
+           U =  U^T ;
+           F =  F^T ;
+           η = η^T  ;
+           ε = ε^T ;
            isAdjunction = record {
                adjoint1 = λ {b} → IsAlgebra.identity (isAlgebra b) ; -- adjoint1
                adjoint2 = adjoint2
@@ -339,14 +342,20 @@
                   EMap (( TMap ε^T ( FObj F^T a )) ∙ ( FMap F^T ( TMap η^T a )) )
                ≈⟨⟩
                   TMap μ a  o FMap T ( TMap η a )
-               ≈⟨ IsMonad.unity2 (isMonad M) ⟩
+               ≈⟨ IsMonad.unity2 M ⟩
                   EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
                ∎
 
 open MResolution
 
-Resolution^T : MResolution A Eilenberg-MooreCategory T U^T F^T {η^T} {ε^T} {μ^T} Adj^T 
+Resolution^T : MResolution A Eilenberg-MooreCategory  ( record { T = T ; η = η ; μ = μ; isMonad = M } )
 Resolution^T = record {
+     UR =  U^T ;
+     FR =  F^T ;
+     ηR =  η^T ;
+     εR =  ε^T ;
+     μR =  μ^T  ;
+     Adj = Adjunction.isAdjunction Adj^T ;
      T=UF = Lemma-EM8;
      μ=UεF  = Lemma-EM11
  }
diff -r d0bc017c6b61 -r a5f2ca67e7c5 free-monoid.agda
--- a/free-monoid.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/free-monoid.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -199,8 +199,6 @@
 
 -- solution
 
-open UniversalMapping
-
 --   [a,b,c] → f(a) ∙ f(b) ∙ f(c)
 Φ :  {a : Obj A } {b : Obj B} ( f : Hom A a (FObj U b) ) →  List a → Carrier b
 Φ {a} {b} f [] = ε b
@@ -236,9 +234,12 @@
 eta :  (a : Obj A) → Hom A a ( FObj U (Generator a) )
 eta  a = λ ( x : a ) →  x :: []
 
-FreeMonoidUniveralMapping : UniversalMapping A B U Generator eta  
+FreeMonoidUniveralMapping : UniversalMapping A B 
 FreeMonoidUniveralMapping = 
     record {
+       U = U ;
+       F = Generator ;
+       η =  eta ;
        _* = λ {a b} → λ f → solution a b f ; 
        isUniversalMapping = record {
              universalMapping = λ {a b f} → universalMapping {a} {b} {f} ; 
@@ -308,8 +309,9 @@
 
 open NTrans
 --   fm-ε b = Φ
+
 fm-ε :  NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor
-fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
+fm-ε =  nat-ε A B FreeMonoidUniveralMapping 
 --   TMap = λ a  →  solution (FObj U a) a (λ x → x ) ;
 --   isNTrans = record {
 --        commute =  commute1 
@@ -337,8 +339,6 @@
      commute1 {a} {b} {f} =  refl   --    λ (x : a ) → f x :: []
         
 
-open Adjunction
-
 -- A = Sets {c}
 -- B = Monoids  
 -- U   underline funcotr
@@ -346,7 +346,7 @@
 -- Eta          x :: []
 -- Epsiron      morph = Φ
 
-adj = UMAdjunction  A B  U Generator eta FreeMonoidUniveralMapping 
+adj = UMAdjunction A B FreeMonoidUniveralMapping 
 
  
 
diff -r d0bc017c6b61 -r a5f2ca67e7c5 kleisli.agda
--- a/kleisli.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/kleisli.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -24,7 +24,7 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ }  where
+                 { M : IsMonad A T η μ }  where
 
 --T(g f) = T(g) T(f)
 
@@ -49,15 +49,14 @@
 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))     -- association law
 
 
-open Monad
 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
                  { a : Obj A } →
-                 ( M : Monad A T η μ )
+                 ( M : IsMonad A T η μ )
     → A [ A [  TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
-Lemma3 = λ m → IsMonad.assoc ( isMonad m )
+Lemma3 = λ m → IsMonad.assoc m
 
 
 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
@@ -69,18 +68,18 @@
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
                  { a : Obj A } →
-                 ( M : Monad A T η μ )
+                 ( M : IsMonad A T η μ )
     →  A [ A [ TMap μ a o TMap η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma5 = λ m → IsMonad.unity1 ( isMonad m )
+Lemma5 = λ m → IsMonad.unity1 m
 
 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
                  { a : Obj A } →
-                 ( M : Monad A T η μ )
+                 ( M : IsMonad A T η μ )
     →  A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-Lemma6 = λ m → IsMonad.unity2 ( isMonad m )
+Lemma6 = λ m → IsMonad.unity2 m
 
 -- Laws of Kleisli Category
 --
@@ -91,6 +90,11 @@
 -- h ○ (g ○ f) = (h ○ g) ○ f  -- assocation law (Lemma9)
 
 -- η(b) ○ f = f
+
+join : (m : IsMonad A T η μ ) → { a b : Obj A } → { c : Obj A } →
+                              ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
+join _ {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
+
 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
                       → A  [ join M (TMap η b) f  ≈ f ]
 Lemma7 {_} {b} f = 
@@ -101,7 +105,7 @@
          A [ TMap μ b  o A [ FMap T ((TMap η b)) o f ] ]  
      ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
         A [ A [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
-     ≈⟨ car ( IsMonad.unity2 ( isMonad M) )  ⟩
+     ≈⟨ car ( IsMonad.unity2 M )  ⟩
         A [  id (FObj T b)   o f ]
      ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
         f
@@ -120,7 +124,7 @@
      A [ TMap μ b  o A [ (TMap η ( FObj T b)) o f ] ] 
   ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
      A [ A [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
-  ≈⟨ car ( IsMonad.unity1 ( isMonad M) ) ⟩
+  ≈⟨ car ( IsMonad.unity1 M ) ⟩
      A [ id (FObj T b)  o f ]
   ≈⟨  IsCategory.identityL (Category.isCategory A)  ⟩
      f
@@ -170,7 +174,7 @@
    ≈⟨ car ( car (
       begin
          ( TMap μ d o TMap μ (FObj T d) )
-      ≈⟨ IsMonad.assoc ( isMonad M) ⟩
+      ≈⟨ IsMonad.assoc M ⟩
          ( TMap μ d o FMap T (TMap μ d) )
       ∎
    )) ⟩
@@ -292,7 +296,7 @@
         identity {a} = let open ≈-Reasoning (A) in
           begin
               TMap μ (a)  o FMap T (TMap η a)
-          ≈⟨ IsMonad.unity2 (isMonad M) ⟩
+          ≈⟨ IsMonad.unity2 M ⟩
              id (FObj T a)
           ∎
         ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ]
@@ -314,7 +318,7 @@
              TMap μ (c)  o (( FMap T ( TMap μ (c)) o FMap T  (FMap T (KMap g)  o (KMap f))))
           ≈⟨ assoc ⟩
              (TMap μ (c)  o ( FMap T ( TMap μ (c)))) o FMap T  (FMap T (KMap g)  o (KMap f))
-          ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
+          ≈⟨ car (sym (IsMonad.assoc M)) ⟩
              (TMap μ (c)  o ( TMap μ (FObj T c))) o FMap T  (FMap T (KMap g)  o (KMap f))
           ≈⟨ sym assoc ⟩
              TMap μ (c)  o (( TMap μ (FObj T c)) o FMap T  (FMap T (KMap g)  o (KMap f)))
@@ -366,7 +370,7 @@
              (FMap T g  o TMap η (b)) o f
           ≈⟨ sym idL ⟩
              id (FObj T c)  o ((FMap T g  o TMap η (b)) o f)
-          ≈⟨ sym (car (IsMonad.unity2 (isMonad M)))  ⟩
+          ≈⟨ sym (car (IsMonad.unity2 M))  ⟩
              (TMap μ c  o FMap T (TMap η c)) o ((FMap T g  o TMap η (b)) o f)
           ≈⟨ sym assoc  ⟩
              TMap μ c  o  ( FMap T (TMap η c) o ((FMap T g  o TMap η (b)) o f) )
@@ -408,7 +412,7 @@
            TMap μ (b)  o ( FMap T (TMap η (b)) o FMap T f)
      ≈⟨ assoc  ⟩
            (TMap μ (b)  o  FMap T (TMap η (b))) o FMap T f
-     ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩
+     ≈⟨ car (IsMonad.unity2 M) ⟩
            id (FObj T b) o FMap T f
      ≈⟨ idL ⟩
            FMap T f 
@@ -464,7 +468,7 @@
               TMap μ b  o  (TMap η (FObj T b) o (TMap μ (b)  o FMap T (KMap f)))
           ≈⟨ assoc ⟩
               (TMap μ b  o  (TMap η (FObj T b))) o (TMap μ (b)  o FMap T (KMap f))
-          ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩
+          ≈⟨ (car (IsMonad.unity1 M)) ⟩
               id (FObj T b) o (TMap μ (b)  o FMap T (KMap f))
           ≈⟨ idL ⟩
               TMap μ b  o FMap T (KMap f) 
@@ -525,8 +529,12 @@
               TMap μ x
           ∎ )
 
-Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
+Adj_T : Adjunction A KleisliCategory 
 Adj_T = record {
+           U = U_T ;
+           F = F_T ;
+           η = nat-η ;
+           ε = nat-ε  ;
            isAdjunction = record {
                adjoint1 = adjoint1 ; 
                adjoint2 = adjoint2
@@ -543,7 +551,7 @@
                   (TMap μ (b)  o (id (FObj T (FObj T b ))))  o ( TMap η ( FObj T b ))
                ≈⟨ car idR ⟩
                   TMap μ (b) o ( TMap η ( FObj T b ))
-               ≈⟨ IsMonad.unity1 (isMonad M) ⟩
+               ≈⟨ IsMonad.unity1 M ⟩
                   id (FObj U_T b)
                ∎ 
            adjoint2 :   {a : Obj A} →
@@ -560,7 +568,7 @@
                   TMap μ a o ((TMap η (FObj T a)) o (TMap η a))
                ≈⟨ assoc  ⟩
                   (TMap μ a o (TMap η (FObj T a))) o (TMap η a)
-               ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩
+               ≈⟨ car (IsMonad.unity1 M) ⟩
                   id (FObj T a) o (TMap η a)
                ≈⟨ idL ⟩
                   TMap η a
@@ -572,8 +580,14 @@
 
 open MResolution
 
-Resolution_T : MResolution A KleisliCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
+Resolution_T : MResolution A KleisliCategory ( record { T = T ; η = η ; μ = μ; isMonad = M } )
 Resolution_T = record {
+      UR = U_T ;
+      FR = F_T ;
+      ηR = nat-η ;
+      εR = nat-ε ;
+      μR = nat-μ ;
+      Adj = Adjunction.isAdjunction Adj_T  ;
       T=UF   = Lemma11;
       μ=UεF  = Lemma12 
   }
diff -r d0bc017c6b61 -r a5f2ca67e7c5 pullback.agda
--- a/pullback.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/pullback.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -235,9 +235,12 @@
 
 limit2couniv :
      ( lim : ( Γ : Functor I A ) → Limit A I Γ )
-     →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ( lim b) )  ( λ b → t0 (lim b)  )
-limit2couniv lim  = record {  -- F             U                            ε
-       _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; -- η
+     →  coUniversalMapping A ( A ^ I ) 
+limit2couniv lim  = record {  
+       F =  KI I ;
+       U =  λ b → a0 ( lim b) ;
+       ε = λ b → t0 (lim b) ;
+       _*' = λ {b} {a} k → limit (isLimit (lim b )) a k ; 
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
            couniquness = couniquness2
@@ -263,43 +266,59 @@
 
 open import Category.Cat
 
-
-open coUniversalMapping
-
 univ2limit :
-     ( U : Obj (A ^ I ) → Obj A )
-     ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K A I (U b)) b )
-     ( univ :  coUniversalMapping A (A ^ I) (KI I) U ε ) →
+     ( univ :  coUniversalMapping A (A ^ I) ) →
      ( Γ : Functor I A ) →   Limit A I Γ 
-univ2limit U ε univ Γ = record {
+univ2limit univ Γ = record {
      a0 = U Γ ;
-     t0 = ε Γ ;
+     t0 = ε ;
      isLimit = record {
              limit = λ a t → limit1 a t ;
              t0f=t = λ {a t i } → t0f=t1 {a} {t} {i}  ;
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
  } where
+     F : Functor A  (A ^ I)
+     F = coUniversalMapping.F univ
+     U : Obj (A ^ I ) → Obj A 
+     U = coUniversalMapping.U univ
+     η : (i : Obj I) → Hom A (U Γ) (FObj (FObj F (U Γ)) i)
+     η i = {!!}
+     ε :  NTrans I A (K A I (U Γ)) Γ 
+     ε  = record {
+         TMap = λ (i : Obj I) → A [ TMap ( coUniversalMapping.ε univ Γ ) i o η i ] ;
+         isNTrans = record { commute = {!!} }
+       }
+     ε' : ( b : Obj (A ^ I ) ) → NTrans I A (FObj F (U b)) b
+     ε' b = coUniversalMapping.ε univ b
+     limit1' :  (a : Obj A) → NTrans I A (FObj F a) Γ → Hom A a (U Γ)
+     limit1' a t = coUniversalMapping._*' univ {_} {a} t
      limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ)
-     limit1 a t = _*' univ {_} {a} t
+     limit1 a t = coUniversalMapping._*' univ {_} {a} (record {
+          TMap = λ (i : Obj I) → A [ TMap t i o {!!} ] ;
+          isNTrans = record { commute = {!!}
+        } } )
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K A I a) Γ}  {i : Obj I} →
-                A [ A [ TMap (ε Γ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap ε i o limit1 a t ] ≈ TMap t i ]
      t0f=t1 {a} {t} {i} =  let  open ≈-Reasoning (A) in begin
-            TMap (ε Γ) i o limit1 a t
+            TMap ε i o limit1 a t
         ≈⟨⟩
-            TMap (ε Γ) i o _*' univ {Γ} {a} t
-        ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
+            TMap ε i o coUniversalMapping._*' univ {Γ} {a} {!!}
+        -- ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {?} {?} ⟩
+        ≈⟨ {!!} ⟩
             TMap t i
         ∎
      limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
-         → ( ∀ { i : Obj I } → A [ A [ TMap  (ε Γ) i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
+         → ( ∀ { i : Obj I } → A [ A [ TMap  ε i o  f ]  ≈ TMap t i ] ) → A [ limit1 a t ≈ f ]
      limit-uniqueness1 {a} {t} {f} εf=t = let  open ≈-Reasoning (A) in begin
-            _*' univ t
-        ≈⟨  ( coIsUniversalMapping.couniquness ( iscoUniversalMapping univ) ) εf=t  ⟩
+            coUniversalMapping._*' univ {!!}
+        ≈⟨ {!!} ⟩
+        -- ≈⟨  ( coIsUniversalMapping.couniquness ( coUniversalMapping.iscoUniversalMapping univ) ) εf=t  ⟩
             f
         ∎
 
 
+
 -- another form of uniqueness of a product
 lemma-p0 :   (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) →
       A [ _×_ prod π1 π2 ≈  id1 A ab  ]
@@ -517,11 +536,8 @@
  
 adjoint-preseve-limit :
      { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit B I Γ ) →
-         { U : Functor B A } { F : Functor A B }
-         { η : NTrans A A identityFunctor ( U ○ F ) }
-         { ε : NTrans B B  ( F ○  U ) identityFunctor } →
-       ( adj : Adjunction A B U F η ε  ) →  Limit A I (U ○ Γ) 
-adjoint-preseve-limit B Γ limitb {U} {F} {η} {ε} adj = record {
+       ( adj : Adjunction A B ) →  Limit A I (Adjunction.U adj ○ Γ) 
+adjoint-preseve-limit B Γ limitb adj = record {
      a0 = FObj U lim ;
      t0 = ta1 B Γ lim tb U ;
      isLimit = record {
@@ -530,6 +546,14 @@
              limit-uniqueness =  λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f
      }
     } where
+         U : Functor B A
+         U = Adjunction.U adj
+         F : Functor A B 
+         F = Adjunction.F adj
+         η : NTrans A A identityFunctor ( U ○ F ) 
+         η = Adjunction.η adj
+         ε : NTrans B B  ( F ○  U ) identityFunctor  
+         ε = Adjunction.ε adj
          ta = ta1 B Γ (a0 limitb) (t0 limitb) U
          tb = t0 limitb
          lim = a0 limitb
diff -r d0bc017c6b61 -r a5f2ca67e7c5 universal-mapping.agda
--- a/universal-mapping.agda	Wed Nov 08 19:57:43 2017 +0900
+++ b/universal-mapping.agda	Sat Nov 11 21:34:58 2017 +0900
@@ -16,22 +16,26 @@
 --
 --
 
-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 {
+      → Adjunction A B → UniversalMapping A B 
+Adj2UM A B adj = record {
+         U = U ;
+         F = FObj F ;
+         η = TMap η ;
          _* = solution  ;
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
                     uniquness = uniqueness
               }
       } where
+         U : Functor B A 
+         U = Adjunction.U adj
+         F : Functor A B 
+         F = Adjunction.F adj
+         η : NTrans A A identityFunctor ( U ○  F ) 
+         η = Adjunction.η adj
+         ε : NTrans B B  ( F ○  U ) identityFunctor 
+         ε = Adjunction.ε adj
          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') } →
@@ -50,7 +54,7 @@
                   (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))  ⟩
+              ≈⟨ car ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj))  ⟩
                   id (FObj U b) o f
               ≈⟨  idL  ⟩
                   f
@@ -76,7 +80,7 @@
                   ( 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 )) ⟩
+              ≈⟨ cdr ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
                   g o id (FObj F a)
               ≈⟨ idR ⟩
                   g
@@ -94,15 +98,20 @@
 --
 
 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 {
+       → UniversalMapping A B → Functor A B
+FunctorF A B um = record {
               FObj = F;
               FMap = myFMap ;
               isFunctor = myIsFunctor
        } where
+    U : Functor B A 
+    U = UniversalMapping.U um
+    F : Obj A → Obj B 
+    F = UniversalMapping.F um
+    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
+    η = UniversalMapping.η um
+    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* _ = UniversalMapping._* um 
     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) ]) ]
@@ -117,19 +126,19 @@
            η 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-id {a} =   ( IsUniversalMapping.uniquness ( UniversalMapping.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 ))  ⟩
+       ≈⟨  ( IsUniversalMapping.universalMapping ( 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-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( UniversalMapping.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) →
@@ -141,18 +150,18 @@
            (( 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 ))  ⟩
+       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( 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 ))  ⟩
+       ≈⟨ car ( IsUniversalMapping.universalMapping ( 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-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( UniversalMapping.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
@@ -166,16 +175,21 @@
 -- 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 {
+                 → (um : UniversalMapping A B )  →
+           NTrans  A A identityFunctor ( UniversalMapping.U um ○ FunctorF A B um )
+nat-η A B um = record {
              TMap = η ; isNTrans = myIsNTrans
        } where
+    U : Functor B A 
+    U = UniversalMapping.U um
+    F : Obj A → Obj B 
+    F = UniversalMapping.F um
+    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
+    η = UniversalMapping.η um
     F' : Functor A B
     F' = FunctorF A B um
+    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* _ = UniversalMapping._* 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
@@ -183,23 +197,28 @@
             (FMap U (FMap F' f))  o  ( η a )
        ≈⟨⟩
             (FMap U ((_* um)  (A [  η b  o f ])))   o  ( η a )
-       ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um ))  ⟩
+       ≈⟨ (IsUniversalMapping.universalMapping ( 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 {
+       → (um : UniversalMapping A B  )  →
+           NTrans B B ( FunctorF A B um ○ UniversalMapping.U um ) identityFunctor
+nat-ε A B um = record {
              TMap = ε ; isNTrans = myIsNTrans
        } where
+    U : Functor B A 
+    U = UniversalMapping.U um
+    F : Obj A → Obj B 
+    F = UniversalMapping.F um
+    η : (a : Obj A) → Hom A a ( FObj U (F a) ) 
+    η = UniversalMapping.η um
     F' : Functor A B
     F' = FunctorF A B um
+    _* : (UniversalMapping A B) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
+    _* _ = UniversalMapping._* 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 ) →
@@ -212,11 +231,11 @@
           ( 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 )) )  ⟩
+       ≈⟨ cdr ((IsUniversalMapping.universalMapping ( 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 )) ) ⟩
+       ≈⟨ car ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩
            id1 A (FObj U b) o FMap U f
        ≈⟨ idL ⟩
             FMap U f
@@ -232,7 +251,7 @@
           (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)) ⟩
+       ≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um)) ⟩
           FMap U f o id (FObj U a )
        ∎
     commute : {a b : Obj B} {f : Hom B a b }
@@ -244,9 +263,9 @@
           ε 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))) ⟩
+       ≈⟨ sym ( ( IsUniversalMapping.uniquness ( UniversalMapping.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)) ⟩
+       ≈⟨ (IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )  (lemma-nat2 a b f)) ⟩
           f o  ((_* um) ( id1 A (FObj U a)))
        ≈⟨⟩
           f o  (ε a)
@@ -260,24 +279,32 @@
 --
 -----
 
-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 {
+UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') →
+       (um : UniversalMapping A B )  →
+              Adjunction A B 
+UMAdjunction A B um = record {
+           U = UniversalMapping.U um ;
+           F = FunctorF A B um ;
+           η = nat-η A B um ;
+           ε = nat-ε A B um ;
            isAdjunction = record {
                adjoint1 = adjoint1 ;
                adjoint2 = adjoint2
            }
        } where
+          U : Functor B A 
+          U = UniversalMapping.U um
           F : Functor A B
           F = FunctorF A B um
           η : NTrans A A identityFunctor ( U ○  F )
           η = nat-η A B um
+          η' : (a : Obj A) → Hom A a ( FObj U (FObj F a) )
+          η' = TMap (nat-η A B um)
           ε : NTrans B B  ( F ○  U ) identityFunctor
           ε = nat-ε A B um
+          _* : UniversalMapping A B →  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
+          _* _ = UniversalMapping._* um
+          isUniversalMapping = UniversalMapping.isUniversalMapping
           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
@@ -409,12 +436,8 @@
                            lemma-2 g h  = let open ≈-Reasoning (A) in car ( right-injective  )
 
 Adj2UO : {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 } →
-                 ( adj : Adjunction A B U F η ε )  → UnityOfOppsite A B U F
-Adj2UO A B {U} {F} {η} {ε} adj = record {
+                 ( adj : Adjunction A B )  → UnityOfOppsite A B (Adjunction.U adj) (Adjunction.F adj)
+Adj2UO A B adj = record {
             right =  right ;
             left  =  left ;
             right-injective =  right-injective  ;
@@ -424,6 +447,14 @@
             r-cong = r-cong ;
             l-cong = l-cong
       } where
+            U : Functor B A 
+            U = Adjunction.U adj
+            F : Functor A B 
+            F = Adjunction.F adj
+            η : NTrans A A identityFunctor ( U ○  F ) 
+            η = Adjunction.η adj
+            ε : NTrans B B  ( F ○  U ) identityFunctor 
+            ε = Adjunction.ε adj
             right  : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b
             right {a} {b} f = B [ TMap ε b o FMap F f ]
             left   : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b   → Hom A a ( FObj U b )
@@ -440,7 +471,7 @@
                          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 )) ⟩
+                     ≈⟨  car  ( IsAdjunction.adjoint1 ( Adjunction.isAdjunction adj )) ⟩
                         id1 A (FObj U b) o f
                      ≈⟨ idL  ⟩
                         f
@@ -457,7 +488,7 @@
                          ( f  o TMap ε ( FObj F a )) o ( FMap F ( TMap η a ))
                      ≈↑⟨ assoc  ⟩
                           f  o ( TMap ε ( FObj F a ) o ( FMap F ( TMap η a )))
-                     ≈⟨  cdr  ( IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
+                     ≈⟨  cdr  ( IsAdjunction.adjoint2 ( Adjunction.isAdjunction adj )) ⟩
                         f o id1 B (FObj F a)
                      ≈⟨ idR  ⟩
                         f
@@ -537,9 +568,12 @@
 UO2UM  : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  ( U : Functor B A )
                  ( F : Functor A B ) →
-                 ( uo : UnityOfOppsite A B U F)  → UniversalMapping A B U (FObj F) ( uo-η-map A B U F uo  )
+                 ( uo : UnityOfOppsite A B U F)  → UniversalMapping A B 
 UO2UM  A B U F uo = record {
          _* = uo-solution A B U F uo  ;
+         U = U ;
+         F = FObj F ;
+         η = uo-η-map A B U F uo  ; 
          isUniversalMapping = record {
                     universalMapping  = universalMapping;
                     uniquness = uniqueness
@@ -641,8 +675,12 @@
                  { U : Functor B A }
                  { F : Functor A B }
                  ( uo : UnityOfOppsite A B U F)
-                    → Adjunction A B U F ( uo-η A B U F uo ) (uo-ε A B U F uo )
+                    → Adjunction A B 
 UO2Adj A B {U} {F} uo = record {
+           U =  U ;
+           F =  F ;
+           η =  uo-η A B U F uo  ;
+           ε =  uo-ε A B U F uo ;
            isAdjunction = record {
                adjoint1 = adjoint1 ;
                adjoint2 = adjoint2