Mercurial > hg > Members > kono > Proof > category

changeset 282:c831abfa9bf4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Sep 2013 17:23:40 +0900
parents dbd2044add2a
children 5492a0681f55
files pullback.agda
diffstat 1 files changed, 113 insertions(+), 67 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Mon Sep 23 13:21:59 2013 +0900
+++ b/pullback.agda	Mon Sep 23 17:23:40 2013 +0900
@@ -11,17 +11,17 @@
 open import HomReasoning
 open import cat-utility
 
--- 
+--
 -- Pullback from equalizer and product
 --         f
 --     a -------> c
---     ^          ^                 
+--     ^          ^
 --  π1 |          |g
 --     |          |
 --    ab -------> b
 --     ^   π2
 --     |
---     | e = equalizer (f π1) (g π1)  
+--     | e = equalizer (f π1) (g π1)
 --     |
 --     d <------------------ d'
 --         k (π1' × π2' )
@@ -30,34 +30,34 @@
 open Product
 open Pullback
 
-pullback-from :  (a b c ab d : Obj A) 
+pullback-from :  (a b c ab d : Obj A)
       ( f : Hom A a c )    ( g : Hom A b c )
       ( π1 : Hom A ab a )  ( π2 : Hom A ab b ) ( e : Hom A d ab )
-      ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g ) 
-      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g 
+      ( eqa : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
+      ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g
           ( A [  π1 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
-          ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] ) 
+          ( A [  π2 o equalizer ( eqa ( A [ f  o π1 ] ) ( A [ g  o π2 ] ){e} )  ] )
 pullback-from  a b c ab d f g π1 π2 e eqa prod =  record {
               commute = commute1 ;
-              p = p1 ; 
-              π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11  {d} {π1'} {π2'} {eq} ; 
-              π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ; 
+              p = p1 ;
+              π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11  {d} {π1'} {π2'} {eq} ;
+              π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21  {d} {π1'} {π2'} {eq} ;
               uniqueness = uniqueness1
-      } where 
+      } where
       commute1 :  A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ]
       commute1 = let open ≈-Reasoning (A) in
              begin
-                    f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) 
+                    f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
              ≈⟨ assoc ⟩
-                    ( f o  π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) 
+                    ( f o  π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
              ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩
-                    ( g o  π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) 
+                    ( g o  π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 ))
              ≈↑⟨ assoc ⟩
-                    g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) 
+                    g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) )
              ∎
-      lemma1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → 
+      lemma1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] →
                       A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ]
-      lemma1  {d'} { π1' } { π2' } eq  = let open ≈-Reasoning (A) in 
+      lemma1  {d'} { π1' } { π2' } eq  = let open ≈-Reasoning (A) in
              begin
                     ( f o π1 ) o (prod × π1') π2'
              ≈↑⟨ assoc ⟩
@@ -72,9 +72,9 @@
                     ( g o π2 ) o (prod × π1') π2'
              ∎
       p1 :  {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d
-      p1 {d'} { π1' } { π2' } eq  = 
+      p1 {d'} { π1' } { π2' } eq  =
          let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) ( lemma1 eq )
-      π1p=π11 :   {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 
+      π1p=π11 :   {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
             A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ]
       π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
              begin
@@ -84,11 +84,11 @@
              ≈↑⟨ assoc ⟩
                       π1 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
              ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
-                      π1 o  (_×_ prod  π1'  π2' ) 
+                      π1 o  (_×_ prod  π1'  π2' )
              ≈⟨ π1fxg=f prod ⟩
                      π1'
              ∎
-      π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → 
+      π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} →
             A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ]
       π2p=π21  {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in
              begin
@@ -98,7 +98,7 @@
              ≈↑⟨ assoc ⟩
                       π2 o ( e o  k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod  π1'  π2' ) (lemma1 eq) )
              ≈⟨ cdr ( ek=h  ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩
-                      π2 o  (_×_ prod  π1'  π2' ) 
+                      π2 o  (_×_ prod  π1'  π2' )
              ≈⟨ π2fxg=g prod ⟩
                      π2'
              ∎
@@ -119,7 +119,7 @@
                 (prod × (  π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p'))
              ≈⟨ ×-cong prod (assoc) (assoc) ⟩
                  (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]))
-                         (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) 
+                         (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])
              ≈⟨ ×-cong prod eq1 eq2 ⟩
                 ((prod × π1') π2')
              ∎ ) ⟩
@@ -147,7 +147,7 @@
 
 open NTrans
 
-record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) 
+record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
      ( a0 : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
   field
      limit :  ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
@@ -157,7 +157,7 @@
          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 I a0 ) Γ 
+  T0 : NTrans I A ( K I a0 ) Γ
   T0 = t0
 
 --------------------------------
@@ -168,13 +168,13 @@
 
 iso-l :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
      ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
-       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
+       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )
       → Hom A a0 a0'
 iso-l  I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0
 
 iso-r :  { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
      ( a0 a0' : Obj A ) (  t0 : NTrans I A ( K I a0 ) Γ ) (  t0' : NTrans I A ( K I a0' ) Γ )
-       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' ) 
+       ( lim : Limit I Γ a0 t0 ) → ( lim' :  Limit I Γ a0' t0' )
       → Hom A a0' a0
 iso-r  I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0'
 
@@ -188,11 +188,11 @@
       ≈↑⟨ limit-uniqueness lim'  ( λ {i} → ( begin
           TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' )
       ≈⟨ assoc  ⟩
-          ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0' 
+          ( TMap t0' i o  limit lim' a0 t0 ) o limit lim a0' t0'
       ≈⟨ car ( t0f=t lim' ) ⟩
-          TMap t0 i o limit lim a0' t0' 
+          TMap t0 i o limit lim a0' t0'
       ≈⟨ t0f=t lim ⟩
-          TMap t0' i 
+          TMap t0' i
       ∎) ) ⟩
            limit lim' a0' t0'
       ≈⟨ limit-uniqueness lim' idR ⟩
@@ -200,7 +200,7 @@
       ∎
 
 
-open import CatExponetial 
+open import CatExponetial
 
 open Functor
 
@@ -213,10 +213,10 @@
       FObj = λ a → K I a ;
       FMap = λ f → record { --  NTrans I A (K I a)  (K I b)
             TMap = λ a → f ;
-            isNTrans = record { 
+            isNTrans = record {
                  commute = λ {a b f₁} → commute1 {a} {b} {f₁} f
             }
-        }  ; 
+        }  ;
         isFunctor = let  open ≈-Reasoning (A) in record {
                ≈-cong   = λ f=g {x} → f=g
              ; identity = refl-hom
@@ -225,12 +225,12 @@
   } where
      commute1 :  {a b : Obj I} {f₁ : Hom I a b} → {a' b' : Obj A} → (f : Hom A a' b' ) →
         A [ A [ FMap (K I b') f₁ o f ] ≈ A [ f o FMap (K I a') f₁ ] ]
-     commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin 
-            FMap (K I b') f₁ o f 
+     commute1 {a} {b} {f₁} {a'} {b'} f = let  open ≈-Reasoning (A) in begin
+            FMap (K I b') f₁ o f
         ≈⟨ idL ⟩
            f
         ≈↑⟨ idR ⟩
-            f o FMap (K I a') f₁ 
+            f o FMap (K I a') f₁
         ∎
 
 
@@ -239,31 +239,31 @@
 -- limit gives co universal mapping ( i.e. adjunction )
 --
 --     F = KI I : Functor A (A ^ I)
---     U = λ b → A0 (lim b {a0 b} {t0 b} 
---     ε = λ b → T0 ( lim b {a0 b} {t0 b} ) 
+--     U = λ b → A0 (lim b {a0 b} {t0 b}
+--     ε = λ b → T0 ( lim b {a0 b} {t0 b} )
 
-limit2couniv : 
+limit2couniv :
      ( lim : ( Γ : Functor I A ) → { a0 : Obj A } { t0 : NTrans I A ( K I a0 ) Γ } → Limit I Γ a0 t0 )
      → ( a0 : ( b : Functor I A ) → Obj A ) ( t0 :  ( b : Functor I A ) → NTrans I A ( K I (a0 b) ) b )
      →  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 ; -- η
        iscoUniversalMapping = record {
-           couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; 
+           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 ]
    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 {a0 b} {t0 b})) i o TMap ( FMap (KI I) (limit (lim b {a0 b} {t0 b}) a f) ) i
         ≈⟨⟩
             TMap (t0 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 ] ) 
+        ( ∀ { 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} {a} {f} {g} lim-g=f  =  let  open ≈-Reasoning (A) in begin
             limit (lim b {a0 b} {t0 b} ) a f
@@ -275,19 +275,19 @@
 
 
 open coUniversalMapping
- 
-univ2limit : 
-     ( U : Obj (A ^ I ) → Obj A ) 
+
+univ2limit :
+     ( U : Obj (A ^ I ) → Obj A )
      ( ε : ( b : Obj (A ^ I ) ) → NTrans I A (K I (U b)) b )
      ( univ :  coUniversalMapping A (A ^ I) (KI I) U (ε) ) →
      ( Γ : Functor I A ) →   Limit I Γ (U Γ) (ε Γ)
 univ2limit U ε univ Γ = 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 
+     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
      limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a (U Γ)
-     limit1 a t = _*' univ {_} {a} t 
+     limit1 a t = _*' univ {_} {a} t
      t0f=t1 :   {a : Obj A} {t : NTrans I A (K I 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
@@ -297,7 +297,7 @@
         ≈⟨ coIsUniversalMapping.couniversalMapping ( iscoUniversalMapping univ) {Γ} {a} {t} ⟩
             TMap t i
         ∎
-     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I a ) Γ } → { f : Hom A a (U Γ)} 
+     limit-uniqueness1 : { a : Obj A } →  { t : NTrans I A ( K I 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
             _*' univ t
@@ -320,33 +320,79 @@
       pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
       ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ product ( λ (i : I) →  A [ (pi i)  o h ] )  ≈  h ]
       ip-cong : {q : Obj A}   → ( qi : (i : I) → Hom A q (ai i) ) → ( qi' : (i : I) → Hom A q (ai i) )
-                → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ] 
+                → ( ∀ (i : I ) →  A [ qi i ≈ qi' i ] ) → A [ product qi ≈ product qi' ]
+
+open IProduct
 
-open IProduct 
+--
+-- limit from equalizer and product
+--
+--      
+--       ai 
+--      ^ ^
+--      | | pi
+--      | |
+--      | p 
+--      | ^ 
+--      | |
+--      | | e = equalizer (f pi) (g pi')
+--      | |
+--       lim <------------------ d'
+--         k ( product pi )
 
-limit-equalizer :  
+open Equalizer
+
+limit-equalizer :
       ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
                   →  IProduct {c₁'} A (Obj I) p ai pi )
-      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g ) 
-     ( Γ : Functor I A ) →   
-     ( lim : Obj A ) 
-     ( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) → 
+      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
+     ( Γ : Functor I A ) →
+     ( lim p : Obj A ) ( e : Hom  A lim p )
+     ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
          NTrans I A (K I lim) Γ
-limit-equalizer prod eqa Γ lim proj = record {
-      TMap = tmap ; 
+limit-equalizer prod eqa Γ lim p e proj = record {
+      TMap = tmap ;
       isNTrans = record {
-          commute = {!!}
+          commute = commute1 
       }
   } where
       tmap : (i : Obj I) → Hom A (FObj (K I lim) i) (FObj Γ i)
-      tmap i = A [ ( proj i )  o equalizer ( eqa (id1 A lim) (A [ FMap Γ (id1 I i) o proj i ] ) (A [ {!!} o {!!} ] )) ]
+      tmap i = A [ ( proj i )  o e ]
+      commute1 :  {a b : Obj I} {f : Hom I a b} →
+        A [ A [ FMap Γ f o tmap a ] ≈ A [ tmap b o FMap (K I lim) f ] ]
+      commute1 {i} {j} {f} = let  open ≈-Reasoning (A) in begin
+             FMap Γ f o tmap i
+        ≈⟨⟩
+             FMap Γ f o ( proj i o e )
+        ≈⟨ assoc ⟩
+             ( FMap Γ f o  proj i ) o e 
+        ≈⟨ {!!} ⟩
+             proj j o e 
+        ≈↑⟨ idR ⟩
+             (proj j o e ) o id1 A lim
+        ≈⟨⟩
+             tmap j o FMap (K I lim) f
+        ∎
 
-limit-from :  
+limit-from :
       ( prod : (p : Obj A) ( ai : Obj I → Obj A )  ( pi : (i : Obj I) → Hom A p ( ai i ) )
                   →  IProduct {c₁'} A (Obj I) p ai pi )
-      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g ) 
-     ( Γ : Functor I A ) →   
-     ( lim : Obj A ) 
-     ( proj : (i : Obj I ) → Hom A lim (FObj Γ i) ) → 
-        Limit I Γ lim ( limit-equalizer prod eqa Γ lim proj )
-limit-from prod eqa lim Γ proj = {!!}
+      ( eqa : {a b c : Obj A} → (e : Hom A c a )  → (f g : Hom A a b)  → Equalizer A e f g )
+     ( Γ : Functor I A ) →
+     ( lim p : Obj A ) ( e : Hom  A lim p )
+     ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
+        Limit I Γ lim ( limit-equalizer prod eqa Γ lim p e proj )
+limit-from prod eqa Γ lim p e proj = 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
+         limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim
+         limit1 a t = k (eqa e {!!} {!!} ) (product ( prod p (FObj Γ)  proj ) (TMap t) ) {!!}
+         t0f=t1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
+                A [ A [ TMap (limit-equalizer prod eqa Γ lim p e proj) i o limit1 a t ] ≈ TMap t i ]
+         t0f=t1 = {!!}  
+         limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} → ({i : Obj I} →
+                A [ A [ TMap (limit-equalizer prod eqa Γ lim p e proj) i o f ] ≈ TMap t i ]) →
+                A [ limit1 a t ≈ f ]
+         limit-uniqueness1 = {!!}