Mercurial > hg > Members > kono > Proof > category

changeset 271:28278175d696

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
limit2adjoint done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Sep 2013 20:40:17 +0900
parents 8ba03259a177
children 5f2b8a5cc115
files pullback.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Sun Sep 22 19:49:38 2013 +0900
+++ b/pullback.agda	Sun Sep 22 20:40:17 2013 +0900
@@ -153,8 +153,8 @@
      limit :  ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0
      t0f=t :  { a : Obj A } → { t : NTrans I A ( K 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 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 ]
+     limit-uniqueness : { a : Obj A } →  { t : NTrans I A ( K 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 I a0 ) Γ 
@@ -185,7 +185,7 @@
   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' i ( begin
+      ≈↑⟨ 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' 
@@ -193,9 +193,9 @@
           TMap t0 i o limit lim a0' t0' 
       ≈⟨ t0f=t lim ⟩
           TMap t0' i 
-      ∎ ) ⟩
+      ∎) ) ⟩
            limit lim' a0' t0'
-      ≈⟨ limit-uniqueness lim' i idR ⟩
+      ≈⟨ limit-uniqueness lim' idR ⟩
            id a0'
       ∎
 
@@ -244,7 +244,7 @@
        _*' = λ {b} {a} k → limit (lim b {a0 b} {t0 b} ) a k ;
        iscoUniversalMapping = record {
            couniversalMapping = λ{ b a f} → couniversalMapping1 {b} {a} {f} ; 
-           couniquness = λ {b a f g } → couniquness1 {b} {a} {f} {g}
+           couniquness = couniquness2
        }
   } where
    couniversalMapping1 :  {b : Obj (A ^ I)} {a : Obj A} {f : Hom (A ^ I) (FObj (KI I) a) b} →
@@ -256,12 +256,15 @@
         ≈⟨ t0f=t (lim b) ⟩
             TMap f i  -- i comes from   ∀{i} → B [ TMap f i  ≈  TMap g i  ]
         ∎
-   couniquness1 : {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} ))} →
-        A ^ I [ A ^ I [ T0 (lim b {a0 b} {t0 b} ) o FMap (KI I) g ] ≈ f ] → A [ limit (lim b {a0 b} {t0 b} ) a f ≈ g ]
-   couniquness1 {b} {a} {f} {g} lim-g=f =  let  open ≈-Reasoning (A) in begin
+   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} {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 ) ? lim-g=f ⟩
+        ≈⟨ limit-uniqueness ( lim b {a0 b} {t0 b} ) lim-g=f ⟩
             g
         ∎
 
 
+
+