Mercurial > hg > Members > kono > Proof > category

changeset 676:faf48511f69d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
two product as in CWM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Nov 2017 11:49:45 +0900
parents 1298c3655ba7
children 3b23eeecd4f8
files SetsCompleteness.agda cat-utility.agda pullback.agda
diffstat 3 files changed, 29 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Nov 03 20:45:46 2017 +0900
+++ b/SetsCompleteness.agda	Sat Nov 04 11:49:45 2017 +0900
@@ -58,15 +58,15 @@
        ; pi  = λ i prod  → pi1 prod i
        ; isIProduct = record {
               iproduct = iproduct1
-            ; pif=q = pif=q
+            ; pif=q = λ {q} {qi} {i} → pif=q {q} {qi} {i}
             ; ip-uniqueness = ip-uniqueness
             ; ip-cong  = ip-cong
        }
    } where
        iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
        iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x  }
-       pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
-       pif=q {q} qi {i} = refl
+       pif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets q (fi i)} → {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ]
+       pif=q {q} {qi} {i} = refl
        ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
        ip-uniqueness = refl
        ipcx : {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x
--- a/cat-utility.agda	Fri Nov 03 20:45:46 2017 +0900
+++ b/cat-utility.agda	Sat Nov 04 11:49:45 2017 +0900
@@ -228,7 +228,8 @@
                     : Set  (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where
            field
               iproduct : {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 ( iproduct qi ) ] ≈  (qi i) ]
+              pif=q :   {q : Obj A}  → { qi : (i : I) → Hom A q (ai i) }
+                  → ∀ { i : I } → A [ A [ ( pi i )  o ( iproduct qi ) ] ≈  (qi i) ]
               ip-uniqueness :  {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (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 [ iproduct qi ≈ iproduct qi' ]
--- a/pullback.agda	Fri Nov 03 20:45:46 2017 +0900
+++ b/pullback.agda	Sat Nov 04 11:49:45 2017 +0900
@@ -329,9 +329,10 @@
 
 limit-ε :
      ( prod :  ( ai : Obj I → Obj A ) →  IProduct A (Obj I) ai )
+     ( aprod :  ( ai : { j k : Obj I} → (Hom I j k)  → Obj A  ) →  ∀{ i j : Obj I} → IProduct A (Hom I i j) ai )
      ( eqa : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A f g )
           → NTrans I A (K A I (equc prod eqa )) Γ
-limit-ε prod eqa = record {
+limit-ε prod aprod eqa = record {
        TMap = λ i → tmap i ; 
        isNTrans = record { commute = commute1 }
    } where
@@ -349,24 +350,29 @@
        e-inv = {!!}
        e-iso : {i j : Obj I} {f : Hom I i j} → A [ A [ equalizer (eqa (A [ FMap Γ f o  proj i ]) ( proj j )) o e-inv ] ≈ id1 A p0 ]
        e-iso = {!!}
-       commute1 :  {i j : Obj I} {f : Hom I i j} →
-         A [ A [ FMap Γ f o tmap i ] ≈ A [ tmap j o FMap (K A I lim) f ] ]
-       commute1 {i} {j} {f} =  let  open ≈-Reasoning (A) in begin
-              FMap Γ f o tmap i 
+       Fcod = λ {j} {k} u →  FObj Γ k
+       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 lim) u ] ]
+       commute1 {j} {k} {u} =  let  open ≈-Reasoning (A) in begin
+              FMap Γ u o tmap j 
          ≈⟨⟩
-              FMap Γ f o ( proj i o e )
+              FMap Γ u o ( proj j o e )
          ≈⟨ assoc ⟩
-              ( FMap Γ f o  proj i ) o e 
+              ( FMap Γ u o  pi (prod (FObj Γ)) j ) o e 
+         ≈↑⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
+             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (FMap Γ)) o  pi (prod (FObj Γ)) j ) o e 
          ≈⟨ {!!} ⟩
-              ((( FMap Γ f o  proj i ) o equalizer (eqa (FMap Γ f o  proj i) ( proj j ))) o {!!} ) o  e
-         ≈⟨ car ( car (fe=ge (isEqualizer (eqa (FMap Γ f o  proj i) ( proj j ))))) ⟩
-              ((proj j o equalizer (eqa (FMap Γ f o  proj i) ( proj j ))) o {!!} ) o  e
+             (( pi (aprod Fcod ) u o iproduct (isIProduct (aprod Fcod)) (λ e → id1 A (FObj Γ (Category.cod I e)))) o  pi (prod (FObj Γ)) k ) o e 
+         ≈⟨ car (car ( pif=q (isIProduct (aprod Fcod )))  ) ⟩
+              ( id1 A (FObj Γ k) o pi (prod (FObj Γ)) k  ) o e 
          ≈⟨ {!!} ⟩
-              proj j o e 
+              ( pi (prod (FObj Γ)) k ) o e 
+         ≈⟨⟩
+              proj k o e 
          ≈↑⟨ idR ⟩
-              (proj j o e ) o id1 A lim
+              (proj k o e ) o id1 A lim
          ≈⟨⟩
-              tmap j o FMap (K A I lim) f
+              tmap k o FMap (K A I lim) u
          ∎
 
 limit-from :
@@ -375,7 +381,7 @@
       → Limit A I Γ 
 limit-from prod eqa = record {
      a0 = equalizer-c p0equ ;
-     t0 = limit-ε prod eqa ; 
+     t0 = limit-ε prod {!!} eqa ; 
      isLimit = record {
              limit = λ a t → limit1 a t ;
              t0f=t = λ {a t i } → t0f=t1  {a} {t} {i} ;
@@ -394,20 +400,20 @@
          limit1 :  (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim
          limit1 a t = let  open ≈-Reasoning (A) in k equ (iproduct prodΓ (TMap t) ) refl-hom
          t0f=t1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {i : Obj I} →
-                A [ A [ TMap (limit-ε prod eqa ) i o limit1 a t ] ≈ TMap t i ]
+                A [ A [ TMap (limit-ε prod {!!} eqa ) i o limit1 a t ] ≈ TMap t i ]
          t0f=t1 {a} {t} {i} = let  open ≈-Reasoning (A) in begin
-                   TMap (limit-ε prod eqa ) i o limit1 a t 
+                   TMap (limit-ε prod {!!} eqa ) i o limit1 a t 
                 ≈⟨⟩
                    ( ( proj i )  o e ) o  k equ (iproduct prodΓ (TMap t) ) refl-hom
                 ≈↑⟨ assoc  ⟩
                     proj i  o ( e  o  k equ (iproduct prodΓ (TMap t) ) refl-hom )
                 ≈⟨ cdr ( ek=h equ) ⟩
                     proj i  o iproduct prodΓ (TMap t)
-                ≈⟨ pif=q prodΓ (TMap t) ⟩
+                ≈⟨ pif=q prodΓ ⟩
                    TMap t i 
                 ∎
          limit-uniqueness1 :  {a : Obj A} {t : NTrans I A (K A I a) Γ} {f : Hom A a lim} 
-                → ({i : Obj I} → A [ A [ TMap (limit-ε prod eqa ) i o f ] ≈ TMap t i ]) →
+                → ({i : Obj I} → A [ A [ TMap (limit-ε prod {!!} eqa ) 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