# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1489217888 -32400
# Node ID fcae3025d9007ef98e67eaadd64e54bbd6892f63
# Parent  265f13adf93b304dccbada0df5dd0bd5ede121a1
fix Limit pu a0 and t0 in record definition

diff -r 265f13adf93b -r fcae3025d900 cat-utility.agda
--- a/cat-utility.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/cat-utility.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -303,31 +303,25 @@
 
 
         record Limit { 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
+               : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
+             a0 : Obj A
+             t0 : NTrans I A ( K A I a0 ) Γ 
              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 } →
                  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 } →
                  A [ A [ TMap t0 i o  f ]  ≈ TMap t i ] ) → A [ limit a t ≈ f ]
-          A0 : Obj A
-          A0 = a0
-          T0 : NTrans I A ( K A I a0 ) Γ
-          T0 = t0
 
         record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
-             limit-c :  ( Γ : Functor I A ) -> Obj A
-             limit-u :  ( Γ : Functor I A ) ->  NTrans I A ( K A I (limit-c Γ )) Γ
-             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ 
 
         record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' )
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
-             limit-c :  ( Γ : Functor I A ) -> Obj A
-             limit-u :  ( Γ : Functor I A )  → NTrans I A ( K A I (limit-c Γ )) Γ
-             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ (limit-c Γ) (limit-u Γ)
+             isLimit :  ( Γ : Functor I A ) -> Limit A I Γ 
 
              product : (a b : Obj A) -> Obj A
              π1 : (a b : Obj A) -> Hom A (product a b ) a
@@ -337,3 +331,8 @@
              equalizer-p : {a b : Obj A} (f g : Hom A a b)  -> Obj A
              equalizer-e : {a b : Obj A} (f g : Hom A a b)  -> Hom A (equalizer-p f g) a
              isEqualizer : {a b : Obj A} (f g : Hom A a b)  -> IsEqualizer A (equalizer-e f g) f g
+          open Limit
+          limit-c :  ( Γ : Functor I A ) -> Obj A
+          limit-c  Γ  = a0 ( isLimit Γ)
+          limit-u :  ( Γ : Functor I A ) ->  NTrans I A ( K A I (limit-c Γ )) Γ
+          limit-u  Γ  = t0 ( isLimit Γ)
diff -r 265f13adf93b -r fcae3025d900 freyd.agda
--- a/freyd.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/freyd.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -49,7 +49,7 @@
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A A)
       (SFS : SmallFullSubcategory A ) → 
-      (PI : PreInitial A (SFSF SFS )) → { a0 : Obj A } → HasInitialObject A (limit-c comp (SFSF SFS))
+      (PI : PreInitial A (SFSF SFS )) → HasInitialObject A (limit-c comp (SFSF SFS))
 initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
@@ -58,35 +58,35 @@
       F = SFSF SFS   
       FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 
       FMap←  = SFSFMap←  SFS
-      a0 : Obj A
-      a0 = limit-c comp F
-      lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ) (limit-u comp Γ)
+      a00 : Obj A
+      a00 = limit-c comp F
+      lim : ( Γ : Functor A A ) → Limit A A Γ 
       lim Γ =  isLimit comp Γ 
-      u : NTrans A A (K A A a0) F
-      u = T0 ( lim F )
+      u : NTrans A A (K A A a00) F
+      u = t0 ( lim F )
       equ : {a b : Obj A} → (f g : Hom A a b)  → IsEqualizer A (equalizer-e comp f g ) f g
       equ f g = Complete.isEqualizer comp f g 
       ep : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
       ep {a} {b} {f} {g} = equalizer-p comp f g
       ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
       ee {a} {b} {f} {g} = equalizer-e comp f g  
-      f : {a : Obj A} → Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
+      f : {a : Obj A} → Hom A  a00 (FObj F  (preinitialObj PI {a} ) ) 
       f {a} = TMap u (preinitialObj PI {a} ) 
-      initialArrow :  ∀( a : Obj A )  →  Hom A a0 a
+      initialArrow :  ∀( a : Obj A )  →  Hom A a00 a
       initialArrow a  = A [ preinitialArrow PI {a}  o f ]
-      equ-fi : { a : Obj A} → {f' : Hom A a0 a} → 
+      equ-fi : { a : Obj A} → {f' : Hom A a00 a} → 
           IsEqualizer A ee ( A [ preinitialArrow PI {a} o  f ] ) f'
       equ-fi  {a} {f'} = equ ( A [ preinitialArrow PI {a} o  f ] ) f'
-      e=id : {e : Hom A a0 a0} → ( {c : Obj A} → A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) → A [ e  ≈ id1 A a0 ]
+      e=id : {e : Hom A a00 a00} → ( {c : Obj A} → A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) → A [ e  ≈ id1 A a00 ]
       e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
             begin
               e
             ≈↑⟨ limit-uniqueness  (lim F) e ( λ {i} → uce=uc ) ⟩
-              limit (lim F) a0 u 
-            ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( λ {i} → idR ) ⟩
-              id1 A a0
+              limit (lim F) a00 u 
+            ≈⟨ limit-uniqueness (lim F) (id1 A a00) ( λ {i} → idR ) ⟩
+              id1 A a00
             ∎
-      kfuc=uc : {c k1 : Obj A} →  {p : Hom A k1 a0} → A [ A [ TMap u  c  o  
+      kfuc=uc : {c k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ TMap u  c  o  
               A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]  
                       ≈ TMap u c ]
       kfuc=uc {c} {k1} {p} =  let open ≈-Reasoning (A) in
@@ -99,13 +99,13 @@
             ≈↑⟨ car  ( full→ SFS ) ⟩
                   FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
             ≈⟨ nat u  ⟩
-                  TMap u c o FMap (K A A a0) (FMap← (TMap u c o p o preinitialArrow PI)) 
+                  TMap u c o FMap (K A A a00) (FMap← (TMap u c o p o preinitialArrow PI)) 
             ≈⟨⟩
-                  TMap u c o id1 A a0
+                  TMap u c o id1 A a00
             ≈⟨ idR ⟩
                  TMap u  c  
             ∎
-      kfuc=1 : {k1 : Obj A} →  {p : Hom A k1 a0} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ]
+      kfuc=1 : {k1 : Obj A} →  {p : Hom A k1 a00} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a00 ]
       kfuc=1 {k1} {p} = e=id ( kfuc=uc )
       -- if equalizer has right inverse, f = g
       lemma2 :  (a b : Obj A) {c : Obj A} ( f g : Hom A a b ) 
@@ -129,14 +129,14 @@
                ≈⟨ idR ⟩
                 g
             ∎
-      lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ]
+      lemma1 : (a : Obj A) (f' : Hom A a00 a) → A [ f' ≈ initialArrow a ]
       lemma1 a f' = let open ≈-Reasoning (A) in 
              sym (
              begin
                  initialArrow a
              ≈⟨⟩
                  preinitialArrow PI {a} o  f
-             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  f ]) f' {ee {a0} {a} {A [ preinitialArrow PI {a} o  f ]} {f'} } (equ-fi )
+             ≈⟨ lemma2 a00 a (A [ preinitialArrow PI {a} o  f ]) f' {ee {a00} {a} {A [ preinitialArrow PI {a} o  f ]} {f'} } (equ-fi )
                       (kfuc=1 {ep} {ee} ) ⟩
                  f'
              ∎  )
diff -r 265f13adf93b -r fcae3025d900 freyd1.agda
--- a/freyd1.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/freyd1.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -17,20 +17,6 @@
 open NTrans
 
 
-tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : 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  ○  Γ)
-tb B I Γ 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 
-                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
-                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
-                 ∎
-               } }
-
 open Complete
 open CommaObj
 open CommaHom
@@ -66,55 +52,42 @@
              A [ A [ FMap (FIA Γ) f o arrow (TMap ta a) ] ≈ A [ arrow (TMap ta b) o FMap (K A I (obj c)) f ] ]
         comm1 {a} {b} {f} = IsNTrans.commute (isNTrans ta )
 
+tb : { c₁' c₂' ℓ' : Level} (B : Category c₁' c₂' ℓ') { c₁ c₂ ℓ : Level} ( I : 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  ○  Γ)
+tb B I Γ 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 
+                 ≈⟨ cdr (IsFunctor.identity (isFunctor U) ) ⟩
+                     TMap (Functor*Nat I C U tb) b o FMap (K C I (FObj U lim)) f
+                 ∎
+               } }
+
+FIC : { I : Category c₁ c₂ ℓ } →  ( Γ : Functor I CommaCategory )  → Functor I C
+FIC {I} Γ = G  ○  (FIA Γ)
+
 NIC : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
      (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I C ( K C I (FObj G (obj c)) ) (G ○ ( FIA Γ) )
-NIC  {I} Γ c ta = record {
-        TMap = λ x → FMap G (TMap ta x )
-        ; isNTrans = record { commute = comm1 }
-    }  where
-          comm1 :  {a b : Obj I} {f : Hom I a b} → 
-                C [ C [ FMap (G ○ FIA Γ) f o FMap G (TMap ta a) ] ≈ C [ FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f ] ] 
-          comm1 {a} {b} {f} = let  open ≈-Reasoning (C) in begin
-                 FMap (G ○ FIA Γ) f o FMap G (TMap ta a)
-              ≈↑⟨ distr G  ⟩
-                 FMap G ( A [ FMap (FIA Γ) f o TMap ta a ] )
-              ≈⟨ fcong G  ( nat ta  ) ⟩
-                 FMap G ( A [ TMap ta b o FMap (K A I (obj c)) f ] )
-              ≈⟨ distr G  ⟩
-                 FMap G (TMap ta b) o FMap G (FMap (K A I (obj c)) f  )
-              ≈⟨ cdr ( IsFunctor.identity (isFunctor G )) ⟩
-                 FMap G (TMap ta b) o id1 C (FObj G (obj c))
-              ≈⟨⟩
-                 FMap G (TMap ta b) o FMap (K C I (FObj G (obj c))) f
-              ∎
+NIC  {I} Γ c ta = tb A I (FIA Γ) (obj c) ta G
 
-
-NIComma : { I : Category c₁ c₂ ℓ } →   ( Γ : Functor I CommaCategory ) 
-     (c : Obj CommaCategory ) ( ta : NTrans I A ( K A I (obj c) ) (FIA Γ) )  → NTrans I CommaCategory ( K CommaCategory I c )  Γ
-NIComma  {I} Γ c ta = record {
-        TMap = λ x → record {
-                 arrow =  TMap ta x
-              ;  comm =  comm1 x
-            }
-        ; isNTrans = record { commute = {!!} }
-    }  where
-        comm1 :  ( x : Obj I ) → C [ C [ FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x) ] ≈ C [ hom (FObj Γ x) o FMap F (TMap ta x) ] ] 
-        comm1 x = let  open ≈-Reasoning (C) in begin
-              FMap G (TMap ta x) o hom (FObj (K CommaCategory I c) x)
-           ≈⟨ {!!} ⟩
-              hom (FObj Γ x) o FMap F (TMap ta x) 
-           ∎
-
-
+LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) 
+    → ( Glimit :  ( Γ : Functor I A ) (lim  : Obj A )
+         → ( limita : Limit A I Γ lim ta ) → Limit C I (G ○ Γ) (FObj G lim) (tb A I Γ lim ta G  ) )
+    → ( lim : Obj CommaCategory ) → ( Γ : Functor I CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I ? ) Γ )
+    → Limit C I (FIC Γ) {!!} ( NIC Γ {!!} (NIA Γ {!!} ta) )
+LimitC  {I} comp Glimit lim Γ ta = Glimit (FIA Γ) {!!} (NIA Γ {!!} ta ) (isLimit comp (FIA Γ))
 
 commaLimit :  { I : Category c₁ c₂ ℓ } →  ( Complete A I) →  ( Γ : Functor I CommaCategory )  →  Obj CommaCategory
 commaLimit {I} comp Γ = record {
       obj = limit-c  comp (FIA Γ)
       ; hom = limitHom
    } where
-       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) {!!})
+       ll =    ( limit (isLimit comp (FIA Γ)) (limit-c  comp (FIA Γ)) (NIA Γ {!!} {!!} )) 
        limitHom : Hom C (FObj F (limit-c comp (FIA Γ ) )) (FObj G (limit-c comp (FIA Γ) ))
-       limitHom = C [ FMap G ll   o C [ {!!} o FMap F ll ] ]
+       limitHom = {!!}
 
 
 commaNat : { I : Category c₁ c₂ ℓ } →   ( comp : Complete A I) →  ( Γ : Functor I CommaCategory ) 
@@ -127,7 +100,7 @@
     } where
         tmap :  (i : Obj I) → Hom CommaCategory (FObj (K CommaCategory I c) i) (FObj Γ i)
         tmap i = record {
-              arrow = A [ arrow ( TMap ta i)  o  A [  {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
+              arrow = A [ arrow ( TMap ta i)  o  A [ {!!} o limit ( isLimit comp (FIA Γ ) ) (obj c) ( NIA Γ c ta ) ] ]
               ; comm = {!!}
           }
         commute : {a b : Obj I} {f : Hom I a b} → 
diff -r 265f13adf93b -r fcae3025d900 limit-to.agda
--- a/limit-to.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/limit-to.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -154,7 +154,7 @@
 
 equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂  ℓ) {a b : Obj A} -> (f g : Hom A a b)  (comp : Complete A TwoCat ) ->
          Hom A ( limit-c comp (IndexFunctor A a b f g)) a
-equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) t0
+equlimit A {a} {b} f g comp = TMap (limit-u comp (IndexFunctor A a b f g)) discrete.t0
 
 lim-to-equ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
       (comp : Complete A TwoCat  )
@@ -175,7 +175,7 @@
          e = equlimit A f g comp
          c : Obj A
          c = limit-c comp Γ
-         lim : Limit A I Γ c ( limit-u comp Γ )
+         lim : Limit A I Γ 
          lim =  isLimit comp  Γ
          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 = IndexNat A f g
@@ -185,9 +185,9 @@
          ek=h d h fh=gh = let open  ≈-Reasoning A in  begin
                     e o k h fh=gh
                 ≈⟨⟩
-                    TMap (limit-u comp Γ) t0  o k h fh=gh
-                ≈⟨ t0f=t lim {d} {inat d h fh=gh } {t0}  ⟩
-                    TMap (inat d h fh=gh) t0
+                    TMap (limit-u comp Γ) discrete.t0  o k h fh=gh
+                ≈⟨ t0f=t lim {d} {inat d h fh=gh } {discrete.t0}  ⟩
+                    TMap (inat d h fh=gh) discrete.t0
                 ≈⟨⟩
                     h
                 ∎
@@ -195,13 +195,13 @@
                        ( fh=gh : A [ A [ f  o  h ] ≈ A [ g  o h ] ]) → A [ A [ e o k' ] ≈ h ] →
                        A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ]
          uniq-nat {t0} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
-                    TMap (limit-u comp Γ) t0 o k'
+                    TMap (limit-u comp Γ) discrete.t0 o k'
                 ≈⟨⟩
                     e o k'
                 ≈⟨ ek'=h ⟩
                     h
                 ≈⟨⟩
-                    TMap (inat d h fh=gh) t0
+                    TMap (inat d h fh=gh) discrete.t0
                 ∎
          uniq-nat {t1} d h k' fh=gh ek'=h =  let open  ≈-Reasoning A in begin
                     TMap (limit-u comp Γ) t1 o k'
@@ -210,7 +210,7 @@
                 ≈⟨⟩
                     ( TMap (limit-u comp Γ) t1  o  FMap (K A I c) arrow-f ) o k'
                 ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩
-                    ( FMap Γ  arrow-f  o TMap (limit-u comp Γ) t0 ) o k'
+                    ( FMap Γ  arrow-f  o TMap (limit-u comp Γ) discrete.t0 ) o k'
                 ≈⟨⟩
                    (f o e ) o k'
                 ≈↑⟨ assoc ⟩
diff -r 265f13adf93b -r fcae3025d900 pullback.agda
--- a/pullback.agda	Sat Mar 11 10:51:12 2017 +0900
+++ b/pullback.agda	Sat Mar 11 16:38:08 2017 +0900
@@ -137,39 +137,39 @@
 open NTrans
 
 iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) (  t0' : NTrans I A ( K A I a0' ) Γ )
-       ( lim : Limit A I Γ a0 t0 ) → ( lim' :  Limit A I Γ a0' t0' )
-      → Hom A a0 a0'
-iso-l  I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
+       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ )
+      → Hom A (a0 lim )(a0 lim')
+iso-l  I Γ  lim lim' = limit lim' (a0 lim) ( t0 lim)
 
 iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) (  t0' : NTrans I A ( K A I a0' ) Γ )
-       ( lim : Limit A I Γ a0 t0 ) → ( lim' :  Limit A I Γ a0' t0' )
-      → Hom A a0' a0
-iso-r  I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
+       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ  )
+      → Hom A (a0 lim') (a0 lim)
+iso-r  I Γ lim lim' = limit lim (a0 lim') (t0 lim')
 
 
 iso-lr :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
-     ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K A I a0 ) Γ ) (  t0' : NTrans I A ( K A I a0' ) Γ )
-       ( lim : Limit A I Γ a0 t0 ) → ( lim' :  Limit A I Γ a0' t0' )  → ∀{ i : Obj I } →
-  A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim'  ]  ≈ id1 A a0' ]
-iso-lr  I Γ a0 a0' t0 t0' lim lim' {i} =  let open ≈-Reasoning (A) in begin
-           limit lim' a0 t0 o limit lim a0' t0'
-      ≈↑⟨ limit-uniqueness lim' ( limit lim' a0 t0 o limit lim a0' t0' )( λ {i} → ( begin
-          TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
+       ( lim : Limit A I Γ ) → ( lim' :  Limit A I Γ  )  →
+       ∀{ 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'
+      ≈⟨⟩
+           limit lim' (a0 lim) ( t0 lim) o  limit lim (a0 lim') (t0 lim')
+      ≈↑⟨ limit-uniqueness lim' ( limit lim' (a0 lim) (t0 lim) o limit lim (a0 lim') (t0 lim') )( λ {i} → ( begin
+          TMap (t0 lim') i o ( limit lim' (a0 lim) (t0 lim) o limit lim (a0 lim') (t0 lim') )
       ≈⟨ assoc  ⟩
-          ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0'
+          ( TMap (t0 lim') i o  limit lim' (a0 lim) (t0 lim) ) o limit lim (a0 lim') (t0 lim')
       ≈⟨ car ( t0f=t lim' ) ⟩
-          TMap t0 i o limit lim a0' t0'
+          TMap (t0 lim)  i o limit lim (a0 lim') (t0 lim')
       ≈⟨ t0f=t lim ⟩
-          TMap t0' i
+          TMap (t0 lim') i
       ∎) ) ⟩
-           limit lim' a0' t0'
-      ≈⟨ limit-uniqueness lim' (id a0') idR ⟩
-           id a0'
+           limit lim' (a0 lim') (t0 lim')
+      ≈⟨ limit-uniqueness lim' (id (a0 lim')) idR ⟩
+           id (a0 lim' )
       ∎
 
 
+
 open import CatExponetial
 
 open Functor
@@ -221,31 +221,31 @@
 --     a0 : Obj A and t0 : NTrans K Γ come from the limit
 
 limit2couniv :
-     ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 t0 )
-     → ( a0 : ( Γ : Functor I A ) → Obj A ) ( t0 :  ( Γ : Functor I A ) → NTrans I A ( K A I (a0 Γ) ) Γ )
-     →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → A0 (lim b {a0 b} {t0 b} ) )  ( λ b → T0 ( lim b {a0 b} {t0 b} ) )
-limit2couniv lim a0 t0 = record {  -- F             U                            ε
-       _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ; -- η
+     ( lim : ( Γ : Functor I A ) → Limit A I Γ )
+     → ( aΓ : ( Γ : Functor I A ) → Obj A ) ( tΓ :  ( Γ : Functor I A ) → NTrans I A ( K A I (aΓ Γ) ) Γ )
+     →  coUniversalMapping A ( A ^ I ) (KI I) (λ b → a0 ( lim b) )  ( λ b → t0 (lim b)  )
+limit2couniv lim aΓ tΓ = record {  -- F             U                            ε
+       _*' = λ {b} {a} k → limit (lim b ) a k ; -- η
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ;
            couniquness = couniquness2
        }
   } where
    couniversalMapping1 :  {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
-        A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b}) o FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ] ≈ f ]
+        A ^ I [ A ^ I [ t0 (lim b) o FMap (KI I) (limit (lim b) a f) ] ≈ f ]
    couniversalMapping1 {b} {a} {f} {i} = let  open ≈-Reasoning (A) in begin
-            TMap (T0 (lim b {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i
+            TMap (t0 (lim b )) i o TMap ( FMap (KI I) (limit (lim b ) a f) ) i
         ≈⟨⟩
-            TMap (t0 b) i o (limit (lim b) a f)
+            TMap (t0 (lim b)) i o (limit (lim b) a f)
         ≈⟨ t0f=t (lim b) ⟩
             TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
         ∎
-   couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (A0 (lim b {a0 b} {t0 b} ))} →
-        ( ∀ { i : Obj I } → A [ A [ TMap (T0 (lim b {a0 b} {t0 b} )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] )
-         → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
+   couniquness2 : {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} {g : Hom A a (a0 (lim b ))} →
+        ( ∀ { i : Obj I } → A [ A [ TMap (t0 (lim b )) i  o TMap ( FMap (KI I) g) i  ] ≈ TMap f i ] )
+         → A [ limit (lim b ) a f ≈ g ]
    couniquness2 {b} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
-            limit (lim b {a0 b} {t0 b} ) a f
-        ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) g lim-g=f ⟩
+            limit (lim b ) a f
+        ≈⟨ limit-uniqueness ( lim b ) g lim-g=f ⟩
             g
         ∎
 
@@ -258,8 +258,10 @@
      ( 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 (ε) ) →
-     ( Γ : Functor I A ) →   Limit A I Γ (U Γ) (ε Γ)
+     ( Γ : Functor I A ) →   Limit A I Γ 
 univ2limit U ε univ Γ = record {
+     a0 = U Γ ;
+     t0 = ε Γ ;
      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
@@ -350,8 +352,10 @@
      ( lim p : Obj A )       -- limit to be made
      ( e : Hom  A lim p )                          -- existing of equalizer
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) )  -- existing of product ( projection actually )
-      → Limit A I Γ lim ( limit-ε eqa lim p e proj )
+      → Limit A I Γ 
 limit-from prod eqa lim p e proj = record {
+     a0 = lim ;
+     t0 = limit-ε eqa lim p e proj ;
      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
@@ -417,18 +421,21 @@
                } }
  
 adjoint-preseve-limit :
-     { c₁' c₂' ℓ' : Level}  (B : Category c₁' c₂' ℓ') ( Γ : Functor I B ) 
-     ( lim : Obj B ) ( tb : NTrans I B ( K B I lim ) Γ ) → ( limitb : Limit B I Γ lim tb ) →
+     { 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 ○ Γ) (FObj U lim) (ta1 B Γ lim tb U ) 
-adjoint-preseve-limit B Γ lim tb limitb {U} {F} {η} {ε} adj = record {
+       ( adj : Adjunction A B U F η ε  ) →  Limit A I (U ○ Γ) 
+adjoint-preseve-limit B Γ limitb {U} {F} {η} {ε} adj = record {
+     a0 = FObj U lim ;
+     t0 = ta1 B Γ lim tb U ;
      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
-         ta = ta1 B Γ lim tb U
+         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 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)) Γ
@@ -458,7 +465,7 @@
                   tfmap a t b o FMap (K B I (FObj F a)) f 
                ∎
           } }
-         limit1 :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U lim)
+         limit1 :  (a : Obj A) → NTrans I A (K A I a) (U ○ Γ) → Hom A a (FObj U (a0 limitb) )
          limit1 a t = A [ FMap U (limit 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} →
                 A [ A [ TMap ta i o limit1 a t ] ≈ TMap t i ]