Mercurial > hg > Members > kono > Proof > category

changeset 509:3e82fb1ce170

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IProduct in Sets done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Mar 2017 17:35:57 +0900
parents 3ce21b2a671a
children 5eb4b69bf541
files SetsCompleteness.agda
diffstat 1 files changed, 38 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Mar 18 16:15:40 2017 +0900
+++ b/SetsCompleteness.agda	Sat Mar 18 17:35:57 2017 +0900
@@ -45,6 +45,12 @@
 
 open iproduct
 
+import Relation.Binary.PropositionalEquality
+-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+≡-cong = Relation.Binary.PropositionalEquality.cong 
+
 
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) 
      → IProduct ( Sets  {  c₂} ) I
@@ -52,8 +58,33 @@
        ai =  fi
        ; iprod = iproduct I fi
        ; pi  = λ i prod  → pi1 prod i
-       ; isIProduct = {!!}
-   }
+       ; isIProduct = record {
+              iproduct = λ {q} qi x → record { pi1 = λ i → (qi i) x  }
+            ; pif=q = pif=q
+            ; 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
+       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
+       ipcx {q} {qi} {qi'} qi=qi x  = 
+              begin
+                record { pi1 = λ i → (qi i) x  }
+             ≡⟨ ≡-cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡-cong ( λ f → f x )  (qi=qi i)  )) ⟩
+                record { pi1 = λ i → (qi' i) x  }
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality 
+                  open ≡-Reasoning 
+       ip-cong  : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1  qi' ]
+       ip-cong {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx qi=qi )
+
+
+
 
 SetsEqualizer :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
 SetsEqualizer f g = record { 
@@ -95,18 +126,19 @@
        cong1 refl =  refl 
 
 
-record Slimit  { c₂ } (I :  Set  c₂)  ( sobj :  Set  c₂ → Set  c₂ ) (smap :  { a b  :   Set  c₂ } ( f : a → b ) →  Set  c₂ ) 
+record Slimit  { c₂ } (I :  Set  c₂)  ( sobj : I → Set  c₂ ) (smap :  { a b  :   Set  c₂ } ( f : a → b ) →  Set  c₂ ) 
            : Set  c₂ where
     field 
-        s-t0 : (i : I ) → sobj ?
+        sm : I → I
+        s-t0 : (i : I ) → sobj i
 
 open Slimit
 
 SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
 SetsLimit { c₂}  = record { 
-           a0 =  Slimit (Obj Sets) ΓObj ΓMap
+           a0 =  Slimit (Obj Sets) {!!} ΓMap
          ; t0 = record { 
-               TMap = λ i → λ lim → s-t0 lim ?
+               TMap = λ i → λ lim → s-t0 lim {!!}
              ; isNTrans = record { commute = {!!} } 
            }
          ; isLimit = record {