Mercurial > hg > Members > kono > Proof > category

changeset 534:a90889cc2988

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introducing snat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Mar 2017 14:24:09 +0900
parents c3dcea3a92a7
children 5d7f8921bac0
files SetsCompleteness.agda
diffstat 1 files changed, 24 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed Mar 29 11:59:59 2017 +0900
+++ b/SetsCompleteness.agda	Wed Mar 29 14:24:09 2017 +0900
@@ -166,59 +166,45 @@
     {i j : I } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( shom← s f ) 
 
-
-record slim   { c₂ }  { I :  Set  c₂ } ( sobj :  I →  Set  c₂ ) 
+record snat   { c₂ }  { I :  Set  c₂ } ( sobj :  I →  Set  c₂ ) 
      ( smap : { i j :  I  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
    field 
-        slim-obj : ( i : I ) → sobj i
-        slim-equ : {i j : I} ( f g : I → I ) → sequ I I f g
+       snmap : ( i : I ) → sobj i 
+       sncommute : { i j : I } → ( f : I → I ) →  smap f ( snmap i )  ≡ snmap j
 
-open slim
+open snat
 
 open import HomReasoning
-
 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 ( SetsLimit-c s Γ ) ) Γ
+    → NTrans C Sets (K Sets C (snat  (ΓObj s Γ) (ΓMap s Γ) ) ) Γ
 SetsNat C I s  Γ  =  record {
-               TMap = λ i →  Sets [ proj i o e ]
+               TMap = λ i →  λ sn →  iid ( snmap sn (small→ s i )  )
              ; isNTrans = record { commute = comm1 }
       } where
-    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 ? ? ? ?
-    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  ( 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=ge0 {!!} ⟩
-          Sets [ proj b o e ] 
-        ≈↑⟨ idR  ⟩
-          Sets [ Sets [ proj b o e ] o id1 Sets ( SetsLimit-c s Γ) ]
-        ≈⟨⟩
-          Sets [ Sets [ proj b o e ] o FMap (K Sets C  (SetsLimit-c s Γ)) f ] 
-       ∎   where
-            open  ≈-Reasoning Sets
+    comm1 :  {a b : Obj C} {f : Hom C a b} →
+        Sets [ Sets [ FMap Γ f o (λ sn → iid (snmap sn (small→ s a))) ] ≈
+        Sets [ (λ sn → iid (snmap sn (small→ s b))) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+    comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
+                 FMap Γ f ( iid (snmap sn (small→ s a)) )
+             ≡⟨ {!!} ⟩
+                iid ( (ΓMap s Γ (shom→ s  f))  ( snmap sn ( small→ s a )) )
+             ≡⟨ ≡cong ( λ y → iid y ) ( sncommute sn (shom→ s  f) )  ⟩
+                 iid (snmap sn (small→ s b))
+             ∎  ) 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 { 
-           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
-         ; t0 = {!!} -- SetsNat C I s Γ
+           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
+         ; t0 = SetsNat C I s Γ
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = {!!}
@@ -226,8 +212,8 @@
            }
        }  where
           a0 : Obj Sets
-          a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
+          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
           e  :  Hom Sets a0 (iproduct I (λ j → ΓObj s Γ j))
-          e  =  λ x → record { pi1  = λ j →  slim-obj x j }
-          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
+          e  =  λ x → record { pi1  = λ j →  snmap x j }
+          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 = {!!}