Mercurial > hg > Members > kono > Proof > category

changeset 533:c3dcea3a92a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use sequ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Mar 2017 11:59:59 +0900
parents d5d7163f2a1d
children a90889cc2988
files SetsCompleteness.agda
diffstat 1 files changed, 16 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed Mar 29 09:30:22 2017 +0900
+++ b/SetsCompleteness.agda	Wed Mar 29 11:59:59 2017 +0900
@@ -102,6 +102,10 @@
 equ  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b  f g ) →  a
 equ  (elem x eq)  = x 
 
+fe=ge0  :  {  c₂ : Level}  {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →  
+     (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
+fe=ge0 (elem x eq )  =  eq
+
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -114,8 +118,6 @@
              ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
              ; uniqueness  = uniqueness
        } where
-           fe=ge0  :  (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
-           fe=ge0 (elem x eq )  =  eq
            fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
            fe=ge  =  extensionality Sets (fe=ge0 ) 
            k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
@@ -178,43 +180,36 @@
 open NTrans
 open IsEqualizer
 
+SetsLimit-c : {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) ) → Obj Sets
+SetsLimit-c {_} {_} {_} {C} {I} s Γ = sequ (slim  (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j)  ) {!!} {!!} 
+
 SetsNat : {  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 Γ)) ) Γ
+    → NTrans C Sets (K Sets C ( SetsLimit-c s Γ ) ) Γ
 SetsNat C I s  Γ  =  record {
                TMap = λ i →  Sets [ proj i o e ]
              ; isNTrans = record { commute = comm1 }
       } where
-    e  :  Hom Sets (slim  (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j))
-    e  =  λ x → record { pi1  = λ j →  slim-obj x j }
+    e  :  Hom Sets  ( SetsLimit-c s Γ ) (iproduct I (λ j → ΓObj s Γ j))
+    e  =  λ x → record { pi1  = λ j →  slim-obj (equ x) j }
     iid :  {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
     iid {i} = FMap Γ ( small-iso s ) 
     proj :  (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
     proj i prod = iid (  pi1 prod ( small→ s i )  )
     equa : {b : Obj Sets } ( e : slim  (ΓObj s Γ) (ΓMap s Γ) → iproduct I (λ j → ΓObj s Γ j) ) → ( f g : Hom Sets (iproduct I (λ j → ΓObj s Γ j)) b ) → 
            IsEqualizer Sets e f g
-    equa e f g = {!!}  -- SetsIsEqualizer ? ? ? ?
-    comm2 :  {a b : Obj C} {f : Hom C a b} → ( x : slim  (ΓObj s Γ) (ΓMap s Γ) ) → (Sets [ FMap Γ f o Sets [ proj a o e ] ]) x ≡ (Sets [ proj b o e ]) x 
-    comm2 {a} {b} {f} x =    begin
-        (FMap Γ f ) ( ( proj a o e )  x )
-      ≡⟨⟩
-        (FMap Γ f ) (  iid ( slim-obj x  (small→ s a) ))
-      ≡⟨ {!!} ⟩
-        iid ( slim-obj x ( small→ s b )  ) 
-      ∎   where
-          open  import  Relation.Binary.PropositionalEquality
-          open ≡-Reasoning
+    equa e f g = {!!} -- SetsIsEqualizer ? ? ? ?
     comm1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
-        Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+        Sets [ Sets [ proj b o e ] o FMap (K Sets C  ( SetsLimit-c s Γ ) ) f ] ]
     comm1 {a} {b} {f} = begin
           Sets [ FMap Γ f o Sets [ proj a o e ]  ]
         ≈⟨  assoc  ⟩
           Sets [ Sets [ FMap Γ f o proj a ]  o e  ]
-        ≈⟨ fe=ge  (equa e ( Sets [ FMap Γ f o proj a ] ) (proj b ))  ⟩
+        ≈⟨ fe=ge0 {!!} ⟩
           Sets [ proj b o e ] 
         ≈↑⟨ idR  ⟩
-          Sets [ Sets [ proj b o e ] o id1 Sets (slim  (ΓObj s Γ) (ΓMap s Γ)) ]
+          Sets [ Sets [ proj b o e ] o id1 Sets ( SetsLimit-c s Γ) ]
         ≈⟨⟩
-          Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
+          Sets [ Sets [ proj b o e ] o FMap (K Sets C  (SetsLimit-c s Γ)) f ] 
        ∎   where
             open  ≈-Reasoning Sets
 
@@ -223,7 +218,7 @@
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
            a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
-         ; t0 = SetsNat C I s Γ
+         ; t0 = {!!} -- SetsNat C I s Γ
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = {!!}