Mercurial > hg > Members > kono > Proof > category

changeset 574:dbb5da4ab08f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Apr 2017 00:55:30 +0900
parents cc67ef472636
children 761df92aa225
files SetsCompleteness.agda
diffstat 1 files changed, 50 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Apr 25 11:24:27 2017 +0900
+++ b/SetsCompleteness.agda	Wed Apr 26 00:55:30 2017 +0900
@@ -53,6 +53,20 @@
 
 open iproduct
 
+iproduct1 : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
+iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x  }
+ipcx : {  c₂ : Level} → (I : Obj (Sets {  c₂})) (fi : I → Obj Sets ) {q :  Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x
+ipcx I fi {q} {qi} {qi'} qi=qi x  = 
+      begin
+        record { proj = λ i → (qi i) x  }
+     ≡⟨ ≡cong ( λ qi → record { proj = qi } ) ( extensionality Sets (λ i → ≈-to-≡  (qi=qi i) x )) ⟩
+        record { proj = λ i → (qi' i) x  }
+     ∎  where
+          open  import  Relation.Binary.PropositionalEquality 
+          open ≡-Reasoning 
+ip-cong  : {  c₂ : Level} → (I : Obj (Sets {  c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 I fi qi ≈ iproduct1  I fi qi' ]
+ip-cong I fi {q} {qi} {qi'} qi=qi  = extensionality Sets ( ipcx I fi qi=qi )
+
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) 
      → IProduct ( Sets  {  c₂} ) I
 SetsIProduct I fi = record {
@@ -60,29 +74,16 @@
        ; iprod = iproduct I fi
        ; pi  = λ i prod  → proj prod i
        ; isIProduct = record {
-              iproduct = iproduct1
+              iproduct = iproduct1 I fi 
             ; pif=q = pif=q
             ; ip-uniqueness = ip-uniqueness
-            ; ip-cong  = ip-cong
+            ; ip-cong  = ip-cong I fi
        }
    } where
-       iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
-       iproduct1 {q} qi x = record { proj = λ i → (qi i) x  }
-       pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 qi ] ≈ qi i ]
+       pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi 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 → proj prod i) o h ]) ≈ h ]
+       ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj 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 { proj = λ i → (qi i) x  }
-             ≡⟨ ≡cong ( λ qi → record { proj = qi } ) ( extensionality Sets (λ i → ≈-to-≡  (qi=qi i) x )) ⟩
-                record { proj = λ 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 )
 
 
         --
@@ -185,55 +186,57 @@
        slequ : { i j : OC } → ( f :  I → I ) →  sequ (iproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) (  λ x → proj x j )
    snmap : OC →  Set  c₂ 
    snmap i = sobj i
-   ipp : ( ( i : OC ) → sobj i ) → iproduct OC sobj
-   ipp qi = record { proj = qi }
+   ipp : {i j : OC } → (f : I → I ) → iproduct OC sobj
+   ipp {i} {j} f = equ ( slequ {i} {j} f )
 
 open slim
 
+lemma-equ :   {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))
+    {i j j' : Obj C } →　 ( f f' : I → I ) 
+    →  (se : slim (ΓObj s Γ) (ΓMap s Γ) )
+    →  proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {j'} f' ) i
+lemma-equ C I s Γ {i} {j} f f' se =  begin
+                 proj ( ipp se f ) i
+             ≡⟨ {!!} ⟩
+                 proj ( ipp se f' ) i
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+
 open import HomReasoning
 open NTrans
 
-lemma-equ : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ) 
-      {a b : Obj C  } { f : I → I }  { se : slim (ΓObj s Γ) (ΓMap s Γ)  }
-          → proj (equ (slequ se {a} {a} (λ x → x))) a ≡ proj (equ (slequ se {a} {b} f )) a 
-lemma-equ C I s Γ {a} {b} {f}  {se} = begin
-                  proj (equ (slequ se {a} {a} (λ x → x))) a
-             ≡⟨ ≡cong ( λ p → proj p a )  (  ≡cong ( λ QIX → record { proj = QIX } ) (  
-                extensionality Sets  ( λ  x  →  ≡cong ( λ qi →　qi x  )  refl
-              ) )) ⟩
-                  proj (equ (slequ se {a} {b} f )) a
-             ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
 
 Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
     → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ)  )) Γ
 Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → proj (equ (slequ se {i} {i} (λ x → x )) ) i
+               TMap = λ i →  λ se → proj ( ipp se {i} {i} (\x -> x) ) i
              ; isNTrans = record { commute = commute1 }
       } where
-         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj (equ (slequ se {a} {a} (λ x → x))) a) ] ≈
-                Sets [ (λ se → proj (equ (slequ se {b} {b} (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
+         commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se  (\x -> x) ) a) ] ≈
+                Sets [ (λ se → proj ( ipp se  (\x -> x) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ]
          commute1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
-                   (Sets [ FMap Γ f o (λ se₁ → proj (equ (slequ se₁ (λ x → x))) a) ]) se
+                   (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se  (\x -> x) ) a) ]) se
              ≡⟨⟩
-                   FMap Γ f (proj (equ (slequ se (λ x → x))) a)
-             ≡⟨  ≡cong ( λ g → FMap Γ g (proj (equ (slequ se (λ x → x))) a))  (sym ( hom-iso s  ) ) ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj (equ (slequ se {a} {a} (λ x → x))) a)
-             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ C I s Γ  )   ⟩
-                   FMap Γ  (hom← s ( hom→ s f))  (proj (equ (slequ se (hom→ s f ))) a)
+                   FMap Γ f (proj ( ipp se {a} {a} (\x -> x) ) a)
+             ≡⟨  ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (\x -> x) ) a))  (sym ( hom-iso s  ) ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {a} (\x -> x) ) a)
+             ≡⟨ ≡cong ( λ g →  FMap Γ  (hom← s ( hom→ s f)) g )  ( lemma-equ  C I s Γ {!!} {!!} se ) ⟩
+                   FMap Γ  (hom← s ( hom→ s f))  (proj ( ipp se {a} {b} (hom→ s f) ) a)
              ≡⟨  fe=ge0 ( slequ se (hom→ s f ) ) ⟩
-                   proj (equ (slequ se ( hom→ s f ) )) b
-             ≡⟨ sym ( lemma-equ C I s Γ )  ⟩
-                   proj (equ (slequ se (λ x → x))) b
+                   proj (ipp se {a} {b} ( hom→ s f  )) b
+             ≡⟨ sym {!!} ⟩
+                   proj (ipp se {b} {b} (λ x → x)) b
              ≡⟨⟩
-                  (Sets [ (λ se₁ → proj (equ (slequ se₁ (λ x → x))) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
+                  (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
 
 
+
 SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
@@ -261,9 +264,9 @@
                 ≡⟨   ≡cong ( λ g → record { proj = λ i → g i  } ) (  extensionality Sets  ( λ  i  →  sym (  ≡cong ( λ e → e x ) cif=t ) ) )  ⟩
                   record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x }
                 ≡⟨⟩
-                  record { proj = λ i →   proj (equ (slequ (f x) {i} {i} (λ x → x )) ) i }
-                ≡⟨ ≡cong ( λ g →   record { proj = λ i →  g i  } ) (  extensionality Sets  ( λ  i  → lemma-equ C I s Γ ))  ⟩
-                  record { proj = λ i →  proj (equ (slequ (f x) f')) i  }
+                  record { proj = λ i →   proj (ipp (f x) {{!!}} {{!!}} (\x -> x) ) i }
+                ≡⟨ ≡cong ( λ g →   record { proj = λ i →  g i  } ) ( extensionality Sets  ( λ  i  →  {!!}) ) ⟩
+                  record { proj = λ i →  proj (ipp (f x) {{!!}} {{!!}} f') i  }
                 ∎   where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning