Mercurial > hg > Members > kono > Proof > category

changeset 290:1f897357ec6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 25 Sep 2013 13:59:56 +0900
parents 7dc163c026b7
children c8e26650ddf9
files pullback.agda
diffstat 1 files changed, 8 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/pullback.agda	Wed Sep 25 13:25:14 2013 +0900
+++ b/pullback.agda	Wed Sep 25 13:59:56 2013 +0900
@@ -318,7 +318,7 @@
    field
       product : {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p
       pif=q :   {q : Obj A}  → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i )  o ( product qi ) ] ≈  (qi i) ]
-      -- special case of product ( qi = pi )
+      -- special case of product ( qi = pi ) ( should b proved from pif=q )
       pif=q1 :   { i : I } → { qi :  Hom A p (ai i) } → A [ pi i ≈  qi ]
       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) }
@@ -349,12 +349,10 @@
 limit-ε :
       ( 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 p : Obj A ) ( e : Hom  A lim p )
      ( proj : (i : Obj I ) → Hom A p (FObj Γ i) ) →
          NTrans I A (K I lim) Γ
-limit-ε prod eqa Γ lim p e proj = record {
+limit-ε prod lim p e proj = record {
       TMap = tmap ;
       isNTrans = record {
           commute = commute1 
@@ -382,11 +380,11 @@
      ( 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 p : Obj A )       -- limit to be made
+     ( 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 I Γ lim ( limit-ε prod eqa Γ lim p e proj )
-limit-from prod eqa Γ lim p e proj = record {
+      → Limit I Γ lim ( limit-ε prod 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
@@ -394,9 +392,9 @@
          limit1 :  (a : Obj A) → NTrans I A (K I a) Γ → Hom A a lim
          limit1 a t = let  open ≈-Reasoning (A) in k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {i : Obj I} →
-                A [ A [ TMap (limit-ε prod eqa Γ lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε prod lim p e proj ) i o limit1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
-                   TMap (limit-ε prod eqa Γ lim p e proj ) i o limit1 a t 
+                   TMap (limit-ε prod lim p e proj ) i o limit1 a t 
                 ≈⟨⟩
                    ( ( proj i )  o e ) o  k (eqa e (id1 A p) (id1 A p )) (product ( prod p (FObj Γ)  proj ) (TMap t) ) refl-hom
                 ≈↑⟨ assoc  ⟩
@@ -407,7 +405,7 @@
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K I a) Γ} {f : Hom A a lim} 
-                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa Γ lim p e proj ) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod lim p e proj ) i o f ] ≈ TMap t i ]) →
                 A [ limit1 a t ≈ f ]
          limit-uniqueness1 {a} {t} {f} lim=t = let  open ≈-Reasoning (A) in begin
                     limit1 a t