changeset 691:917e51be9bbf

change argument of Limit and K
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Nov 2017 09:56:40 +0900
parents 3d41a8edbf63
children 3ca3b5a4ab45
files SetsCompleteness.agda cat-utility.agda freyd.agda freyd1.agda freyd2.agda limit-to.agda pullback.agda
diffstat 7 files changed, 165 insertions(+), 166 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/SetsCompleteness.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -52,7 +52,7 @@
 open iproduct
 
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
-     → IProduct ( Sets  {  c₂} ) I ai
+     → IProduct I ( Sets  {  c₂} ) ai
 SetsIProduct I fi = record {
        iprod = iproduct I fi
        ; pi  = λ i prod  → pi1 prod i
@@ -193,14 +193,14 @@
 open NTrans
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )
-    → NTrans C Sets (K Sets C (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
+    → NTrans C Sets (K C Sets (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
 Cone C I s  Γ  =  record {
                TMap = λ i →  λ sn →  snmap sn i
              ; isNTrans = record { commute = comm1 }
       } where
     comm1 :  {a b : Obj C} {f : Hom C a b} →
         Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
-        Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+        Sets [ (λ sn →  (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
     comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
                  FMap Γ f  (snmap sn  a )
              ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( hom-iso s  )) ⟩
@@ -214,9 +214,9 @@
                   open ≡-Reasoning
 
 
-SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) )
-    → Limit Sets C Γ
-SetsLimit {c₁} C I s Γ = record {
+SetsLimit : {  c₁ c₂ ℓ : Level} ( I :  Set  c₁ ) ( C : Category c₁ c₂ ℓ )  ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) )
+    → Limit C Sets Γ
+SetsLimit {c₁} I C s Γ = record {
            a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)
          ; t0 = Cone C I s Γ
          ; isLimit = record {
@@ -225,13 +225,13 @@
              ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
-          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I)
+          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I)
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
           comm2 {a} {x} t f =  ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) )
-          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
+          limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))
           limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
               sncommute = λ i j f → comm2 t f }
-          t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
+          t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
           t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
                  ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x
              ≡⟨⟩
@@ -239,7 +239,7 @@
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-          limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} →
+          limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} →
                 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
           limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
@@ -277,7 +277,7 @@
 
 SetsCompleteness : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C
 SetsCompleteness {c₁} {c₂} C I s  =  record {
-         climit = λ Γ → SetsLimit {c₁} C I s Γ
+         climit = λ Γ → SetsLimit {c₁} I C s Γ
       ;  cequalizer = λ {a} {b} f g → record {  equalizer-c = sequ a b f g ;
                 equalizer = ( λ e → equ e ) ;
                 isEqualizer =  SetsIsEqualizer a b f g }
--- a/cat-utility.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/cat-utility.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -221,7 +221,7 @@
         -- product on arbitrary index
         --
 
-        record IsIProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( I : Set c)
+        record IsIProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ )  
               ( p  : Obj A )                       -- product
               ( ai : I → Obj A )                   -- families
               ( pi :  (i : I ) → Hom A p ( ai i ) ) -- projections
@@ -249,11 +249,11 @@
                    iproduct qi

 
-        record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )  ( I : Set c) (ai : I → Obj A) : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
+        record IProduct { c c₁ c₂ ℓ : Level} ( I : Set c) ( A : Category c₁ c₂ ℓ )   (ai : I → Obj A) : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
             field
               iprod :  Obj A
               pi : (i : I ) → Hom A iprod  ( ai i )  
-              isIProduct :  IsIProduct A I iprod  ai  pi  
+              isIProduct :  IsIProduct I A iprod  ai  pi  
 
 
         -- Pullback
@@ -299,9 +299,9 @@
 
         -- Constancy Functor
 
-        K : { c₁' c₂' ℓ' : Level}  (A : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( I : Category c₁'' c₂'' ℓ'' )
+        K : { c₁' c₂' ℓ' : Level}  (I : Category c₁' c₂' ℓ') { c₁'' c₂'' ℓ'' : Level} ( A : Category c₁'' c₂'' ℓ'' )
             → ( a : Obj A ) → Functor I A
-        K A I a = record {
+        K I A a = record {
               FObj = λ i → a ;
               FMap = λ f → id1 A a ;
                 isFunctor = let  open ≈-Reasoning (A) in record {
@@ -312,65 +312,65 @@
           }
 
 
-        record IsLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-             (a0 : Obj A ) (t0 : NTrans I A ( K A I a0 ) Γ  ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
+        record IsLimit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+             (a0 : Obj A ) (t0 : NTrans I A ( K I A a0 ) Γ  ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
-             limit :  ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0
-             t0f=t :  { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } →
+             limit :  ( a : Obj A ) → ( t : NTrans I A ( K I A a ) Γ ) → Hom A a a0
+             t0f=t :  { a : Obj A } → { t : NTrans I A ( K I A a ) Γ } → ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  limit a t ]  ≈ TMap t i ]
-             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
+             limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } →
                  A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
 
-        record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
+        record Limit { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level}  ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
                : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              a0 : Obj A
-             t0 : NTrans I A ( K A I a0 ) Γ 
-             isLimit : IsLimit A I Γ a0 t0 
+             t0 : NTrans I A ( K I A a0 ) Γ 
+             isLimit : IsLimit I A Γ a0 t0 
 
-        LimitNat : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} 
+        LimitNat : { c₁' c₂' ℓ' : Level} (I : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( B : Category c₁ c₂ ℓ ) { c₁'' c₂'' ℓ'' : Level} 
              ( C : Category c₁'' c₂'' ℓ'' ) 
              ( Γ : Functor I B )
-             ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) →
-                 ( U : Functor B C)  → NTrans I C ( K C I (FObj U lim) ) (U  ○  Γ)
-        LimitNat B I C Γ lim tb U = record {
+             ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) →
+                 ( U : Functor B C)  → NTrans I C ( K I C (FObj U lim) ) (U  ○  Γ)
+        LimitNat I B C Γ lim tb U = record {
                        TMap  = TMap (Functor*Nat I C U tb) ;
                        isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (C) in begin
                              FMap (U ○ Γ) f o TMap (Functor*Nat I C U tb) a
                          ≈⟨ nat ( Functor*Nat I C U tb ) ⟩
-                             TMap (Functor*Nat I C U tb) b o FMap (U ○ K B I lim) f
+                             TMap (Functor*Nat I C U tb) b o FMap (U ○ K I B lim) f
                          ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
-                             TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
+                             TMap (Functor*Nat I C U tb) b o FMap (K I C (FObj U lim)) f

                        } }
 
         open Limit
-        record LimitPreserve { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) 
+        record LimitPreserve { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' ) 
              { c₁'' c₂'' ℓ'' : Level} ( C : Category c₁'' c₂'' ℓ'' ) 
               (G : Functor A C) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁'' ⊔ c₂'' ⊔ ℓ'' )) where
           field
-             preserve :  ( Γ : Functor I A ) → ( limita : Limit A I Γ  ) → 
-                   IsLimit C I (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat A I C Γ (a0 limita ) (t0 limita) G )
-          plimit :  { Γ : Functor I A } → ( limita : Limit A I Γ  ) →  Limit C I (G  ○ Γ  )
+             preserve :  ( Γ : Functor I A ) → ( limita : Limit I A Γ  ) → 
+                   IsLimit I C (G ○ Γ) (FObj G (a0 limita ) ) (LimitNat I A C Γ (a0 limita ) (t0 limita) G )
+          plimit :  { Γ : Functor I A } → ( limita : Limit I A Γ  ) →  Limit I C (G  ○ Γ )
           plimit {Γ} limita =  record { a0 = (FObj G (a0 limita ))
-             ; t0 =  LimitNat A I C Γ (a0 limita ) (t0 limita) G
+             ; t0 =  LimitNat I A C Γ (a0 limita ) (t0 limita) G
              ; isLimit = preserve Γ limita }
 
-        record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
+        record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( I : Category c₁ c₂ ℓ ) ( A : Category c₁' c₂' ℓ' )
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
-             climit :  ( Γ : Functor I A ) → Limit A I Γ 
+             climit :  ( Γ : Functor I A ) → Limit I A Γ 
 
         record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
-             climit :  ( Γ : Functor I A ) → Limit A I Γ 
-             cproduct : ( I : Set c₁' ) (fi : I → Obj A )  → IProduct A I fi -- c₁ should be a free level
+             climit :  ( Γ : Functor I A ) → Limit I A Γ 
+             cproduct : ( I : Set c₁' ) (fi : I → Obj A )  → IProduct I A fi -- c₁ should be a free level
              cequalizer : {a b : Obj A} (f g : Hom A a b)  → Equalizer A  f g
           open Limit
           limit-c :  ( Γ : Functor I A ) → Obj A
           limit-c  Γ  = a0 ( climit Γ)
-          limit-u :  ( Γ : Functor I A ) →  NTrans I A ( K A I (limit-c Γ )) Γ
+          limit-u :  ( Γ : Functor I A ) →  NTrans I A ( K I A (limit-c Γ )) Γ
           limit-u  Γ  = t0 ( climit Γ)
           open Equalizer
           equalizer-p : {a b : Obj A} (f g : Hom A a b)  → Obj A
--- a/freyd.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/freyd.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -50,7 +50,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A  (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
+      (PI : PreInitial A  (SFSF SFS )) → IsInitialObject A (limit-c comp (SFSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ {a} f → lemma1 a f
--- a/freyd1.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/freyd1.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -51,13 +51,13 @@
 --- Get a nat on A from a nat on CommaCategory
 --
 NIA : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
-     (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ )  → NTrans I A ( K A I (obj c) )  (FIA Γ)
+     (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K I CommaCategory c ) Γ )  → NTrans I A ( K I A (obj c) )  (FIA Γ)
 NIA  {I} Γ c ta = record {
         TMap = λ x → arrow (TMap ta x )
         ; isNTrans = record { commute = comm1 }
     }  where
         comm1 : {a b : Obj I} {f : Hom I a b} → 
-             A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
+             A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K I A (obj c)) f ] ]
         comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
 
 
@@ -67,19 +67,19 @@
 --
 LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
     → ( Γ : Functor I CommaCategory ) 
-    → ( glimit :  LimitPreserve A I  C G )
-    → Limit C I (G  ○  (FIA Γ)) 
+    → ( glimit :  LimitPreserve I A C G )
+    → Limit I C (G  ○  (FIA Γ)) 
 LimitC  {I} comp Γ glimit  = plimit glimit (climit comp (FIA Γ))
 
 tu :  { I : Category c₁ c₂ ℓ } →  ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-    →   NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G  ○  (FIA Γ))
+    →   NTrans I C (K I C (FObj F (limit-c comp (FIA Γ)))) (G  ○  (FIA Γ))
 tu {I} comp Γ = record {
       TMap  = λ i →  C [ hom ( FObj Γ i ) o  FMap F ( TMap (t0 ( climit comp (FIA Γ)))  i) ]
     ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
   } where
         commute : {a b : Obj I} {f : Hom I a b}   →
               C [ C [ FMap (G  ○  (FIA Γ)) f o C [ hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ))) a) ] ] 
-            ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f ] ]
+            ≈ C [ C [ hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b) ] o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f ] ]
         commute  {a} {b} {f} =  let  open ≈-Reasoning (C) in begin
              FMap (G  ○  (FIA Γ)) f o ( hom (FObj Γ a) o FMap F (TMap (t0 ( climit comp (FIA Γ)))  a ))
          ≈⟨⟩
@@ -95,7 +95,7 @@
          ≈⟨⟩
               hom (FObj Γ b) o ( FMap F (A [ FMap (FIA Γ)  f  o TMap (t0 ( climit comp (FIA Γ)))  a ] ) )
          ≈⟨ cdr ( fcong F ( IsNTrans.commute (isNTrans (t0 ( climit comp (FIA Γ)))  ))) ⟩
-              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K A I (a0 (climit comp (FIA Γ)))) f ] ))
+              hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o FMap (K I A (a0 (climit comp (FIA Γ)))) f ] ))
          ≈⟨⟩
               hom (FObj Γ b) o ( FMap F ( A [ (TMap (t0 ( climit comp (FIA Γ))) b) o id1 A (limit-c comp (FIA Γ)) ] ))
          ≈⟨ cdr ( distr F ) ⟩
@@ -103,14 +103,14 @@
          ≈⟨ cdr ( cdr ( IsFunctor.identity (isFunctor F) ) ) ⟩
               hom (FObj Γ b) o ( FMap F (TMap (t0 ( climit comp (FIA Γ))) b) o id1 C (FObj F (limit-c comp (FIA Γ))))
          ≈⟨ assoc ⟩
-             ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K C I (FObj F (limit-c comp (FIA Γ)))) f
+             ( hom (FObj Γ b) o FMap F (TMap (t0 ( climit comp (FIA Γ))) b)) o FMap (K I C (FObj F (limit-c comp (FIA Γ)))) f

 limitHom :  { I : Category c₁ c₂ ℓ } →  (comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-    → ( glimit :  LimitPreserve A I C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
+    → ( glimit :  LimitPreserve I A C G ) → Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
 limitHom comp Γ glimit = limit (isLimit (LimitC comp Γ glimit  )) (FObj F ( limit-c  comp (FIA Γ))) (tu comp Γ )
 
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  
-    → ( glimit :  LimitPreserve A I C G )
+    → ( glimit :  LimitPreserve I A C G )
     →  Obj CommaCategory
 commaLimit {I} comp Γ glimit = record {
       obj = limit-c  comp (FIA Γ)
@@ -119,8 +119,8 @@
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
-     → ( glimit :   LimitPreserve A I C G )
-     → NTrans I CommaCategory (K CommaCategory I (commaLimit {I} comp Γ glimit))  Γ
+     → ( glimit :   LimitPreserve I A C G )
+     → NTrans I CommaCategory (K I CommaCategory (commaLimit {I} comp Γ glimit))  Γ
 commaNat {I} comp  Γ glimit = record {
        TMap = λ x → record {
               arrow =  TMap ( limit-u comp (FIA Γ ) ) x 
@@ -129,10 +129,10 @@
        ; isNTrans = record { commute = comm2 }
     } where
        comm1 : (x : Obj I )  →
-              C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x) ] 
+              C [ C [ FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x) ] 
             ≈ C [ hom (FObj Γ x) o FMap F (TMap (limit-u comp (FIA Γ)) x) ] ] 
        comm1 x =  let  open ≈-Reasoning (C) in begin
-              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K CommaCategory I (commaLimit comp Γ glimit)) x)
+              FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (FObj (K I CommaCategory (commaLimit comp Γ glimit)) x)
          ≈⟨⟩
               FMap G (TMap (limit-u comp (FIA Γ)) x) o hom (commaLimit comp Γ glimit) 
          ≈⟨⟩
@@ -146,23 +146,23 @@

        comm2 : {a b : Obj I} {f : Hom I a b} →
           CommaCategory [ CommaCategory [ FMap Γ f o record { arrow = TMap (limit-u comp (FIA Γ)) a ; comm = comm1 a } ]
-          ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K CommaCategory I (commaLimit comp Γ glimit)) f ] ]
+          ≈ CommaCategory [ record { arrow = TMap (limit-u comp (FIA Γ)) b ; comm = comm1 b } o FMap (K I CommaCategory (commaLimit comp Γ glimit)) f ] ]
        comm2 {a} {b} {f} =  let  open ≈-Reasoning (A) in begin
               FMap (FIA Γ) f  o TMap (limit-u comp (FIA Γ)) a 
          ≈⟨ IsNTrans.commute (isNTrans (limit-u comp (FIA Γ)))   ⟩
-              TMap (limit-u comp (FIA Γ)) b  o FMap (K A I (limit-c comp (FIA Γ))) f 
+              TMap (limit-u comp (FIA Γ)) b  o FMap (K I A (limit-c comp (FIA Γ))) f 

 
 gnat :  { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory )
-     →  (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → 
-              NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ)
+     →  (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a)  Γ ) → 
+              NTrans I C (K I C (FObj F (obj a))) (G ○ FIA Γ)
 gnat {I} Γ a t = record {
        TMap = λ i → C [  hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ]
       ; isNTrans = record { commute = λ {x y f} → comm1 x y f }
     } where
        comm1 :  (x y : Obj I) (f : Hom I x y ) →
                 C [ C [ FMap (G ○ FIA Γ) f o C [ hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x) ] ]
-                ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K C I (FObj F (obj a))) f ] ]
+                ≈ C [ C [ hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ] o FMap (K I C (FObj F (obj a))) f ] ]
        comm1 x y f =  let  open ≈-Reasoning (C) in begin
              FMap (G ○ FIA Γ) f o ( hom (FObj Γ x) o FMap F (TMap (NIA Γ a t) x  ))
          ≈⟨⟩
@@ -180,12 +180,12 @@
          ≈⟨ cdr ( fcong F ( IsCategory.identityR (Category.isCategory A)))  ⟩
               hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y)  
          ≈↑⟨ idR ⟩
-             ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K C I (FObj F (obj a))) f
+             ( hom (FObj Γ y) o FMap F (TMap (NIA Γ a t) y) ) o FMap (K I C (FObj F (obj a))) f

 
 
 comma-a0 :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
+     → ( glimit :   LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a)  Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit)
 comma-a0  {I} comp Γ glimit a t = record {
        arrow  = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
      ; comm = comm1
@@ -243,7 +243,7 @@

 
 comma-t0f=t :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) (i : Obj I )
+     → ( glimit :   LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a)  Γ ) (i : Obj I )
      →   CommaCategory [ CommaCategory [ TMap (commaNat comp Γ glimit) i o comma-a0 comp Γ glimit a t ] ≈ TMap t i ]
 comma-t0f=t  {I} comp Γ glimit a t i = let  open ≈-Reasoning (A) in begin
              TMap ( limit-u comp (FIA Γ ) ) i o limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA  {I} Γ a t )
@@ -252,7 +252,7 @@

 
 comma-uniqueness :  { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory )
-     → ( glimit :   LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a)  Γ ) 
+     → ( glimit :   LimitPreserve I A C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K I CommaCategory a)  Γ ) 
      →  ( f :  Hom CommaCategory a  (commaLimit comp Γ glimit)) 
      →   ( ∀ { i : Obj I } → CommaCategory [ CommaCategory [ TMap ( commaNat {  I} comp Γ glimit ) i o  f ]  ≈ TMap t i ] )
      → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ]
@@ -263,9 +263,9 @@

 
 hasLimit : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
-    → ( glimit :   LimitPreserve A I C G )
+    → ( glimit :   LimitPreserve I A C G )
     → ( Γ : Functor I CommaCategory ) 
-    → Limit CommaCategory I Γ 
+    → Limit I CommaCategory Γ 
 hasLimit {I} comp glimit Γ = record {
      a0 = commaLimit {I} comp Γ glimit ;
      t0 = commaNat {  I} comp Γ glimit  ;
--- a/freyd2.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/freyd2.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -100,27 +100,27 @@
 
 YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
       (b : Obj A ) 
-      (Γ : Functor I A) (limita : Limit A I Γ) →
-        IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
+      (Γ : Functor I A) (limita : Limit I A Γ) →
+        IsLimit I Sets (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat I A Sets Γ (a0 limita) (t0 limita) (Yoneda A b))
 YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record {
          limit = λ a t → ψ a t
        ; t0f=t = λ {a t i} → t0f=t0 a t i
        ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 
     } where 
-      hat0 :  NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
-      hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)
+      hat0 :  NTrans I Sets (K I Sets (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ)
+      hat0 = LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)
       haa0 : Obj Sets
       haa0 = FObj (Yoneda A b) (a0 lim)
-      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ
+      ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) → NTrans I A (K I A b ) Γ
       ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where
          commute1 :  {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} →
-                A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ]  ]
+                A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K I A b) f ]  ]
          commute1  {a₁} {b₁} {f} = let open ≈-Reasoning A in begin
                  FMap Γ f o TMap t a₁ x
              ≈⟨⟩
                  ( ( FMap (Yoneda A b  ○ Γ ) f )  *  TMap t a₁ ) x
              ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩
-                 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x
+                 ( TMap t b₁ * ( FMap (K I Sets a) f ) ) x
              ≈⟨⟩
                  ( TMap t b₁ * id1 Sets a ) x
              ≈⟨⟩
@@ -128,15 +128,15 @@
              ≈↑⟨ idR ⟩
                  TMap t b₁ x o id1 A b
              ≈⟨⟩
-                 TMap t b₁ x o FMap (K A I b) f 
+                 TMap t b₁ x o FMap (K I A b) f 

-      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ))
+      ψ  :  (X : Obj Sets)  ( t : NTrans I Sets (K I Sets X) (Yoneda A b ○ Γ))
           →  Hom Sets X (FObj (Yoneda A b) (a0 lim))
       ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b )
-      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I)
-           → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
+      t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)) (i : Obj I)
+           → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ]
       t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
-                 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t  ] ) x
+                 ( Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t  ] ) x
              ≈⟨⟩
                 FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ))
              ≈⟨⟩ -- FMap (Hom A b ) f g  = A [ f o g  ]
@@ -148,8 +148,8 @@
              ≈⟨⟩
                  TMap t i x
              ∎  ))
-      limit-uniqueness0 :  {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} →
-        ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) →
+      limit-uniqueness0 :  {a : Obj Sets} {t : NTrans I Sets (K I Sets a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} →
+        ({i : Obj I} → Sets [ Sets [ TMap (LimitNat I A Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) →
         Sets [ ψ a t ≈ f ]
       limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x →  ≈-≡ A ( begin 
                   ψ a t x
@@ -164,9 +164,9 @@
              ∎  ))
 
 
-YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)
-       (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) 
-YonedaFpreserveLimit A I b = record {
+YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (I : Category c₁ c₂ ℓ) (A : Category c₁ c₂ ℓ)
+       (b : Obj A ) → LimitPreserve I A Sets (Yoneda A b) 
+YonedaFpreserveLimit I A b = record {
        preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim
    } 
 
@@ -181,14 +181,14 @@
 
 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (a : Obj A )
-      → IsInitialObject  ( K (Sets) A * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
+      → IsInitialObject  ( K A Sets * ↓ (Yoneda A a) ) ( record  { obj = a ; hom = λ x → id1 A a } )
 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record {
            initial =  λ b → initial0 b
          ; uniqueness =  λ f → unique f
      } where
          commaCat : Category  (c₂ ⊔ c₁) c₂ ℓ
-         commaCat = K Sets A * ↓ Yoneda A a
-         initObj  : Obj (K Sets A * ↓ Yoneda A a)
+         commaCat = K A Sets * ↓ Yoneda A a
+         initObj  : Obj (K A Sets * ↓ Yoneda A a)
          initObj = record { obj = a ; hom = λ x → id1 A a }
          comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] )  x ≡ hom b x
          comm2 b OneObj = let open ≈-Reasoning A in  ≈-≡ A ( begin
@@ -200,13 +200,13 @@
              ≈⟨ idR ⟩
                 hom b OneObj 
              ∎  )
-         comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ]
+         comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K A Sets *) (hom b OneObj) ] ]
          comm1 b = let open ≈-Reasoning Sets in begin
                 FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a )
              ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩
                 hom b 
              ≈⟨⟩
-                hom b o FMap (K Sets A *) (hom b OneObj) 
+                hom b o FMap (K A Sets *) (hom b OneObj) 

          initial0 : (b : Obj commaCat) →
             Hom commaCat initObj b
@@ -214,12 +214,12 @@
                 arrow = hom b OneObj
               ; comm = comm1 b }
          -- what is comm f ?
-         comm-f :  (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
+         comm-f :  (b : Obj (K A Sets * ↓ (Yoneda A a))) (f : Hom (K A Sets * ↓ Yoneda A a) initObj b)
             → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
-               ≈ Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ] 
+               ≈ Sets [ hom b  o  FMap  (K A Sets *) (arrow f) ]  ] 
          comm-f b f = comm f
-         unique : {b : Obj (K Sets A * ↓ Yoneda A a)}  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
-                → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
+         unique : {b : Obj (K A Sets * ↓ Yoneda A a)}  (f : Hom (K A Sets * ↓ Yoneda A a) initObj b)
+                → (K A Sets * ↓ Yoneda A a) [ f ≈ initial0 b ]
          unique {b} f = let open ≈-Reasoning A in begin
                 arrow f
              ≈↑⟨ idR ⟩
@@ -229,7 +229,7 @@
              ≈⟨⟩
                ( Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
              ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩
-               ( Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ) OneObj
+               ( Sets [ hom b  o  FMap  (K A Sets *) (arrow f) ]  ) OneObj
              ≈⟨⟩
                 hom b OneObj

@@ -244,19 +244,19 @@
 
 
 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
-   → Hom Sets (FObj (K Sets A *) b) (FObj U b)
+   → Hom Sets (FObj (K A Sets *) b) (FObj U b)
 ub A U b x OneObj = x
 ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b )
-   → Obj ( K Sets A * ↓ U)
+   → Obj ( K A Sets * ↓ U)
 ob A U b x = record { obj = b ; hom = ub A U b x}
 fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )  {a b : Obj A} (f : Hom A a b) (x : FObj U a )
-   → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
+   → Hom ( K A Sets * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) )
 fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x }
   where
         fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y
         fArrowComm1 a b f x OneObj = refl
         fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
-         Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ]
+         Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K A Sets *) f ] ]
         fArrowComm a b f x = extensionality Sets ( λ y → begin 
                 ( Sets [ FMap U f o hom (ob A U a x) ] ) y 
              ≡⟨⟩
@@ -276,8 +276,8 @@
 
 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
      (U : Functor A (Sets {c₂}) )
-     ( i : Obj ( K (Sets) A * ↓ U) )
-     (In : IsInitialObject ( K (Sets) A * ↓ U) i ) 
+     ( i : Obj ( K A Sets * ↓ U) )
+     (In : IsInitialObject ( K A Sets * ↓ U) i ) 
        → Representable A U (obj i)
 UisRepresentable A U i In = record {
         repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } }
@@ -294,7 +294,7 @@
                  A [ f o arrow (initial In (ob A U a y)) ]
              ≡⟨⟩
                  A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ]
-             ≡⟨  ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y  o initial In (ob A U a y)] ) ) ⟩
+             ≡⟨  ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K A Sets * ↓ U) [ fArrow A U f y  o initial In (ob A U a y)] ) ) ⟩
                 arrow (initial In (ob A U b (FMap U f y) ))
              ≡⟨⟩
                 (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y
@@ -339,7 +339,7 @@
                 tmap2 b o FMap (Yoneda A (obj i)) f 

       iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * )
-         → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z 
+         → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K A Sets *) y ] ) z 
       iso0 x y  OneObj = refl
       iso→  : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ]
       iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin
@@ -368,19 +368,19 @@
 
 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I )
      (U : Functor A B )
-     (i :  (b : Obj B) → Obj ( K B A b ↓ U) )
-     (In :  (b : Obj B) → IsInitialObject ( K B A b ↓ U) (i b) ) 
+     (i :  (b : Obj B) → Obj ( K A B b ↓ U) )
+     (In :  (b : Obj B) → IsInitialObject ( K A B b ↓ U) (i b) ) 
         where
 
    tmap-η : (y : Obj B)  → Hom B y (FObj U (obj (i y)))
    tmap-η  y = hom (i y) 
 
-   sobj  : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U 
+   sobj  : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaObj (K A B a) U 
    sobj {a} {b} f = record {obj = b; hom =  f } 
-   solution : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f)
+   solution : {a : Obj B} {b : Obj A}  → ( f : Hom B a (FObj U b) ) → CommaHom (K A B a) U (i a) (sobj f)
    solution {a} {b} f = initial (In a) (sobj f)
 
-   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K B A a ↓ U)
+   ηf : (a b  : Obj B)  → ( f : Hom B a b ) → Obj ( K A B a ↓ U)
    ηf a b f  = sobj ( B [ tmap-η b o f ]  )
 
    univ : {a : Obj B} {b : Obj A}  → (f : Hom B a (FObj U b))
@@ -388,7 +388,7 @@
    univ {a} {b} f = let open ≈-Reasoning B in begin
         FMap U (arrow (solution f)) o tmap-η a 
       ≈⟨ comm (initial (In a) (sobj f))  ⟩
-        hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f)))
+        hom (sobj f) o FMap (K A B a) (arrow (initial (In a) (sobj f)))
       ≈⟨ idR ⟩
         f 

@@ -402,7 +402,7 @@
       ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩
         g 
       ∎  where
-         comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ]
+         comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K A B a) g ] ]
          comm1 = let open ≈-Reasoning B in sym idR
 
    UM : UniversalMapping B A U 
--- a/limit-to.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/limit-to.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -110,7 +110,7 @@
 IndexNat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
         →  {a b : Obj A}      (f g : Hom A  a b )
     (d : Obj A) → (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]   →
-        NTrans TwoCat  A (K A TwoCat  d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
+        NTrans TwoCat  A (K TwoCat A d) (IndexFunctor {c₁} {c₂} {ℓ} A a b f g)
 IndexNat {c₁} {c₂} {ℓ} A {a} {b} f g d h fh=gh = record {
     TMap = λ x → nmap x d h ;
     isNTrans = record {
@@ -120,11 +120,11 @@
          I = TwoCat  {c₁} {c₂}
          Γ : Functor I A
          Γ = IndexFunctor {c₁} {c₂} {ℓ} A a b f g
-         nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x)
+         nmap :  (x : Obj I ) ( d : Obj (A)  ) (h : Hom A d a ) → Hom A (FObj (K I A d) x) (FObj Γ x)
          nmap t0 d h = h
          nmap t1 d h = A [ f o  h ]
          commute1 : {x y : Obj I}  {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) →  A [ A [ f  o  h ] ≈ A [ g  o h ] ]
-                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ]
+                 → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K I A d) f' ] ]
          commute1  {t0} {t1} {arrow-f}  d h fh=gh =  let open  ≈-Reasoning A in begin
                     f o h
                 ≈↑⟨ idR ⟩
@@ -153,13 +153,13 @@

 
 
-equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} → (f g : Hom A a b)  (lim : Limit A TwoCat (IndexFunctor A a b f g) ) →
+equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} → (f g : Hom A a b)  (lim : Limit TwoCat A (IndexFunctor A a b f g) ) →
          Hom A (a0 lim) a
 equlimit A {a} {b} f g lim = TMap (Limit.t0 lim) discrete.t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
         →  {a b : Obj A}  (f g : Hom A  a b )
-       (lim : Limit A TwoCat (IndexFunctor A a b f g) )
+       (lim : Limit TwoCat A (IndexFunctor A a b f g) )
         → IsEqualizer A (equlimit A f g lim) f g
 lim-to-equ {c₁} {c₂} {ℓ} A {a} {b} f g lim =  record {
         fe=ge =  fe=ge0
@@ -175,7 +175,7 @@
          e = equlimit A f g lim
          c : Obj A
          c = a0 lim
-         inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ
+         inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K I A d) Γ
          inat = IndexNat A f g
          fe=ge0 : A [ A [ f o (equlimit A f g lim ) ] ≈ A [ g o (equlimit A f g lim ) ] ]
          fe=ge0 = let open  ≈-Reasoning A in  begin
@@ -183,7 +183,7 @@
                 ≈⟨⟩
                     FMap  Γ arrow-f o TMap (Limit.t0 lim) discrete.t0
                 ≈⟨  IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-f} ⟩ 
-                    TMap (Limit.t0 lim) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} ) (a0 lim)) id-t0
+                    TMap (Limit.t0 lim) discrete.t1 o FMap (K (TwoCat {c₁} {c₂} ) A (a0 lim)) id-t0
                 ≈↑⟨ IsNTrans.commute ( isNTrans (Limit.t0 lim)) {discrete.t0} {discrete.t1} {arrow-g} ⟩ 
                     FMap  Γ arrow-g o TMap (Limit.t0 lim) discrete.t0
                 ≈⟨⟩
@@ -218,7 +218,7 @@
                 ≈↑⟨ car (idR) ⟩
                     ( TMap (Limit.t0 lim) t1  o  id c ) o k'
                 ≈⟨⟩
-                    ( TMap (Limit.t0 lim) t1  o  FMap (K A I c) arrow-f ) o k'
+                    ( TMap (Limit.t0 lim) t1  o  FMap (K I A c) arrow-f ) o k'
                 ≈↑⟨ car ( nat1 (Limit.t0 lim) arrow-f ) ⟩
                     ( FMap Γ  arrow-f  o TMap (Limit.t0 lim) discrete.t0 ) o k'
                 ≈⟨⟩
@@ -245,22 +245,22 @@
 open DiscreteHom
 
 plimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set  c₁) 
-      →  ( Γ : Functor (DiscreteCat  S ) A ) → (lim : Limit A ( DiscreteCat  S ) Γ )  → Obj A
+      →  ( Γ : Functor (DiscreteCat  S ) A ) → (lim : Limit ( DiscreteCat  S ) A Γ )  → Obj A
 plimit A S Γ lim = a0 lim
 
 discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) →  (DiscreteCat S)  [ f  ≈  id1 (DiscreteCat S) a ]
 discrete-identity  f =   refl
 
 pnat :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  (S : Set  c₁)  
-    → (Γ : Functor (DiscreteCat  S ) A )
+    → (Γ : Functor (DiscreteCat S) A )
     →  {q : Obj A }  ( qi : (i : Obj ( DiscreteCat  S)) → Hom A q (FObj Γ i) )
-    → NTrans (DiscreteCat S )A (K A (DiscreteCat S) q) Γ
+    → NTrans (DiscreteCat S )A (K (DiscreteCat S) A q) Γ
 pnat  A S Γ {q} qi  = record {
         TMap = qi ; 
         isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }
     } where
-        commute :  {a b : Obj (DiscreteCat  S) } {f : Hom ( DiscreteCat  S)  a b} →
-                A [ A [ FMap Γ f o qi a ] ≈ A [ qi  b o FMap (K A (DiscreteCat  S )q) f ] ]
+        commute :  {a b : Obj (DiscreteCat  S) } {f : Hom (DiscreteCat S)  a b} →
+                A [ A [ FMap Γ f o qi a ] ≈ A [ qi  b o FMap (K (DiscreteCat  S) A q) f ] ]
         commute {a} {b} {f} with discrete f
         commute {a} {.a} {f} | refl =  let open  ≈-Reasoning A in  begin
                   FMap Γ f o qi a
@@ -273,20 +273,19 @@
                 ≈↑⟨ idR ⟩
                    qi  a o id q
                 ≈⟨⟩
-                   qi  a o FMap (K A (DiscreteCat S) q) f
+                   qi  a o FMap (K (DiscreteCat S) A q) f

 
 lim-to-product :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set  c₁ )
-        →  ( Γ : Functor (DiscreteCat  S ) A )  
-        → (lim : Limit A ( DiscreteCat S ) Γ )
-        → IProduct  A (Obj ( DiscreteCat  S ) ) 
+        →  ( Γ : Functor (DiscreteCat S) A )  
+        → (lim : Limit (DiscreteCat S) A Γ )
+        → IProduct  (Obj (DiscreteCat S))  A (FObj Γ)
 lim-to-product A S Γ lim = record {
-          ai  = λ i → FObj Γ i
-          ; iprod = plimit A S Γ lim
+          iprod = plimit A S Γ lim
           ; pi =  λ  i →   TMap (Limit.t0 lim) i 
           ; isIProduct =  record {
               iproduct = λ {q} qi → iproduct {q} qi ;
-              pif=q =  λ {q } qi { i } → pif=q {q} qi {i}  ;
+              pif=q =  λ {q} {qi} {i} → pif=q {q} qi {i}  ;
               ip-uniqueness  = λ  {q } { h } → ip-uniqueness {q} {h} ;
               ip-cong  =  λ {q } { qi }  { qi' } qi=qi' → ip-cong  {q} {qi} {qi'} qi=qi'
           }
--- a/pullback.agda	Sun Nov 12 01:29:47 2017 +0900
+++ b/pullback.agda	Sun Nov 12 09:56:40 2017 +0900
@@ -150,18 +150,18 @@
 open NTrans
 
 iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ )
+       ( lim : Limit I A Γ ) → ( lim' :  Limit I A Γ )
       → Hom A (a0 lim )(a0 lim')
 iso-l  I Γ  lim lim' = limit (isLimit lim') (a0 lim) ( t0 lim)
 
 iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ  )
+       ( lim : Limit I A Γ ) → ( lim' :  Limit I A Γ  )
       → Hom A (a0 lim') (a0 lim)
 iso-r  I Γ lim lim' = limit (isLimit lim) (a0 lim') (t0 lim')
 
 
 iso-lr :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ  )  →
+       ( lim : Limit I A Γ ) → ( lim' :  Limit I A Γ  )  →
        ∀{ i : Obj I } → A [ A [ iso-l I Γ lim lim' o iso-r I Γ  lim lim'  ]  ≈ id1 A (a0 lim') ]
 iso-lr  I Γ lim lim' {i} =  let open ≈-Reasoning (A) in begin
            iso-l I Γ lim lim' o iso-r I Γ lim lim'
@@ -193,8 +193,8 @@
 
 KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) →  Functor A ( A ^ I )
 KI { c₁'} {c₂'} {ℓ'} I = record {
-      FObj = λ a → K A I a ;
-      FMap = λ f → record { --  NTrans I A (K A I a)  (K A I b)
+      FObj = λ a → K I A a ;
+      FMap = λ f → record { --  NTrans I A (K I A a)  (K I A b)
             TMap = λ a → f ;
             isNTrans = record {
                  commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
@@ -207,13 +207,13 @@
         }
   } where
      commute1 :  {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
-        A [ A [ FMap (K A I b') f₁ o f ] ≈ A [ f o FMap (K A I a') f₁ ] ]
+        A [ A [ FMap (K I A b') f₁ o f ] ≈ A [ f o FMap (K I A a') f₁ ] ]
      commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin
-            FMap (K A I b') f₁ o f
+            FMap (K I A b') f₁ o f
         ≈⟨ idL ⟩
            f
         ≈↑⟨ idR ⟩
-            f o FMap (K A I a') f₁
+            f o FMap (K I A a') f₁

 
 
@@ -234,7 +234,7 @@
 --     a0 : Obj A and t0 : NTrans K Γ come from the limit
 
 limit2couniv :
-     ( lim : ( Γ : Functor I A ) → Limit A I Γ )
+     ( lim : ( Γ : Functor I A ) → Limit I A Γ )
      →  coUniversalMapping A ( A ^ I ) (KI I) 
 limit2couniv lim  = record {  
        U = λ b → a0 ( lim b) ;
@@ -267,7 +267,7 @@
 
 univ2limit :
      ( univ :   coUniversalMapping A (A ^ I) (KI I) ) →
-     ( Γ : Functor I A ) →   Limit A I Γ 
+     ( Γ : Functor I A ) →   Limit I A Γ 
 univ2limit univ Γ = record {
      a0 = (coUniversalMapping.U univ ) Γ  ;
      t0 = (coUniversalMapping.ε univ ) Γ  ;
@@ -283,7 +283,7 @@
      ε b = coUniversalMapping.ε univ b
      limit1 :  (a : Obj A) → NTrans I A (FObj (KI I) a) Γ → Hom A a (U Γ)
      limit1 a t = coUniversalMapping._*' univ {_} {a} t
-     t0f=t1 :   {a : Obj A} {t : NTrans I A (K A I a) Γ}  {i : Obj I} →
+     t0f=t1 :   {a : Obj A} {t : NTrans I A (K I A a) Γ}  {i : Obj 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
@@ -292,7 +292,7 @@
         ≈⟨ coIsUniversalMapping.couniversalMapping ( coUniversalMapping.iscoUniversalMapping univ) {Γ} {a} {t} ⟩
             TMap t i

-     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a (U Γ)}
+     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I A a ) Γ } → { f : Hom A a (U Γ)}
          → ( ∀ { 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
             coUniversalMapping._*' univ t
@@ -355,9 +355,9 @@
 Homprod {j} {k} u = record {hom-j = j ; hom-k = k ; hom = u}
 
 limit-from :
-     ( prod :  {c : Level} { I : Set c } → ( ai : I → Obj A ) →  IProduct A I ai )
+     ( prod :  {c : Level} { I : Set c } → ( ai : I → Obj A ) →  IProduct I A ai )
      ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
-      → Limit A I Γ 
+      → Limit I A Γ 
 limit-from prod eqa = record {
      a0 = d ;
      t0 = cone-ε ; 
@@ -389,15 +389,15 @@
          -- projection of the product of Hom I
          μ  : {j k : Obj I} → (u : Hom I j k ) → Hom A (iprod (prod Fcod)) (Fcod (Homprod u))
          μ  u = pi (prod Fcod ) (Homprod u) 
-         cone-ε :  NTrans I A (K A I (equalizer-c equ-ε ) ) Γ
+         cone-ε :  NTrans I A (K I A (equalizer-c equ-ε ) ) Γ
          cone-ε = record {
                TMap = λ i → tmap i ; 
                isNTrans = record { commute = commute1 }
            } where
-               tmap : (i : Obj I) → Hom A (FObj (K A I d) i) (FObj Γ i)
+               tmap : (i : Obj I) → Hom A (FObj (K I A d) i) (FObj Γ i)
                tmap i = A [ proj i o e ] 
                commute1 :  {j k : Obj I} {u : Hom I j k} →
-                 A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K A I d) u ] ]
+                 A [ A [ FMap Γ u o tmap j ] ≈ A [ tmap k o FMap (K I A d) u ] ]
                commute1 {j} {k} {u} =  let  open ≈-Reasoning (A) in begin
                       FMap Γ u o tmap j 
                  ≈⟨⟩
@@ -419,12 +419,12 @@
                  ≈↑⟨ idR ⟩
                       (proj k o e ) o id1 A d
                  ≈⟨⟩
-                      tmap k o FMap (K A I d) u
+                      tmap k o FMap (K I A d) u

          --  an arrow to our product of Obj I ( is an equalizer because of commutativity of t )
-         h : {a : Obj A} → (t : NTrans I A (K A I a) Γ ) → Hom A a p0
+         h : {a : Obj A} → (t : NTrans I A (K I A a) Γ ) → Hom A a p0
          h t = iproduct prodΓ (TMap t) 
-         fh=gh : (a : Obj A) → (t : NTrans I A (K A I a) Γ ) →
+         fh=gh : (a : Obj A) → (t : NTrans I A (K I A a) Γ ) →
             A [ A [ g o h t ] ≈ A [ f o h t ] ]
          fh=gh a t = let  open ≈-Reasoning (A) in begin
                   g o h t
@@ -456,9 +456,9 @@
                 ≈⟨ ip-uniqueness (isIProduct (prod Fcod)) ⟩
                   f o h t

-         cone1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a d
+         cone1 :  (a : Obj A) → NTrans I A (K I A a) Γ → Hom A a d
          cone1 a t =  k equ (h t) ( fh=gh a t )
-         t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
+         t0f=t1 :  {a : Obj A} {t : NTrans I A (K I A a) Γ} {i : Obj I} →
                 A [ A [ TMap cone-ε  i o cone1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
                    TMap cone-ε  i o cone1 a t 
@@ -471,7 +471,7 @@
                 ≈⟨ pif=q prodΓ ⟩
                    TMap t i 

-         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a d} 
+         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I A a) Γ} {f : Hom A a d} 
                 → ({i : Obj I} → A [ A [ TMap cone-ε  i o f ] ≈ TMap t i ]) →
                 A [ cone1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
@@ -504,22 +504,22 @@
 open import Category.Cat
 
 ta1 : { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) 
-     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → 
-         ( U : Functor B A)  → NTrans I A ( K A I (FObj U lim) ) (U  ○  Γ)
+     ( lim : Obj B ) ( tb : NTrans I B ( K I B lim ) Γ ) → 
+         ( U : Functor B A)  → NTrans I A ( K I A (FObj U lim) ) (U  ○  Γ)
 ta1 B Γ lim tb U = record {
                TMap  = TMap (Functor*Nat I A U tb) ; 
                isNTrans = record { commute = λ {a} {b} {f} → let  open ≈-Reasoning (A) in begin
                      FMap (U ○ Γ) f o TMap (Functor*Nat I A U tb) a 
                  ≈⟨ nat ( Functor*Nat I A U tb ) ⟩
-                     TMap (Functor*Nat I A U tb) b o FMap (U ○ K B I lim) f 
+                     TMap (Functor*Nat I A U tb) b o FMap (U ○ K I B lim) f 
                  ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
-                     TMap (Functor*Nat I A U tb) b o FMap (K A I (FObj U lim)) f
+                     TMap (Functor*Nat I A U tb) b o FMap (K I A (FObj U lim)) f

                } }
  
 adjoint-preseve-limit :
-     { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit B I Γ ) →
-       ( adj : Adjunction A B ) →  Limit A I (Adjunction.U adj ○ Γ) 
+     { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) ( limitb : Limit I B Γ ) →
+       ( adj : Adjunction A B ) →  Limit I A (Adjunction.U adj ○ Γ) 
 adjoint-preseve-limit B Γ limitb adj = record {
      a0 = FObj U lim ;
      t0 = ta1 B Γ lim tb U ;
@@ -540,9 +540,9 @@
          ta = ta1 B Γ (a0 limitb) (t0 limitb) U
          tb = t0 limitb
          lim = a0 limitb
-         tfmap : (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K B I (FObj F a)) i) (FObj Γ i)
+         tfmap : (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → (i : Obj I) → Hom B (FObj (K I B (FObj F a)) i) (FObj Γ i)
          tfmap a t i  = B [ TMap ε (FObj Γ i) o FMap F (TMap t i) ]
-         tF :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) →  NTrans I B (K B I (FObj F a)) Γ
+         tF :  (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) →  NTrans I B (K I B (FObj F a)) Γ
          tF a t = record {
              TMap = tfmap a t ; 
              isNTrans = record { commute = λ {a'} {b} {f} → let  open ≈-Reasoning (B) in begin
@@ -558,20 +558,20 @@
                ≈↑⟨ cdr ( distr F ) ⟩
                   TMap ε (FObj Γ b) o ( FMap F (A [ FMap U (FMap Γ f) o TMap t a' ] ) )
                ≈⟨ cdr ( fcong F (nat t) ) ⟩
-                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o FMap (K A I a) f ])
+                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o FMap (K I A a) f ])
                ≈⟨⟩
-                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o id1 A (FObj (K A I a) b) ])
+                  TMap ε (FObj Γ b) o  FMap F (A [ TMap t b o id1 A (FObj (K I A a) b) ])
                ≈⟨ cdr ( fcong F (idR1 A)) ⟩
                   TMap ε (FObj Γ b) o  FMap F (TMap t b )
                ≈↑⟨ idR ⟩
-                  ( TMap ε (FObj Γ b)  o  FMap F (TMap t b))  o  id1 B (FObj F (FObj (K A I a) b))
+                  ( TMap ε (FObj Γ b)  o  FMap F (TMap t b))  o  id1 B (FObj F (FObj (K I A a) b))
                ≈⟨⟩
-                  tfmap a t b o FMap (K B I (FObj F a)) f 
+                  tfmap a t b o FMap (K I B (FObj F a)) f 

           } }
-         limit1 :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) )
+         limit1 :  (a : Obj A) → NTrans I A (K I A a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) )
          limit1 a t = A [ FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a ]
-         t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {i : Obj I} →
+         t0f=t1 :  {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {i : Obj I} →
                 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in  begin
                  TMap ta i o limit1 a t 
@@ -599,7 +599,7 @@
                  TMap t i

          -- ta = TMap (Functor*Nat I A U tb) , FMap U ( TMap tb i )  o f  ≈ TMap t i
-         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) (U ○ Γ)} {f : Hom A a (FObj U lim)} 
+         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I A a) (U ○ Γ)} {f : Hom A a (FObj U lim)} 
                 → ({i : Obj I} → A [ A [ TMap ta i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in  begin