Mercurial > hg > Members > kono > Proof > category

changeset 531:66cad3cb3a66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Mar 2017 22:25:07 +0900
parents 89af55191ec6
children d5d7163f2a1d
files SetsCompleteness.agda
diffstat 1 files changed, 34 insertions(+), 42 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 28 22:10:52 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 22:25:07 2017 +0900
@@ -177,27 +177,47 @@
 
 open NTrans
 
-SetsNat : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
-    → (lim p : Obj Sets  ) → (e  : Hom Sets  lim p )
-    → NTrans C Sets (K Sets C lim) Γ
-SetsNat C I s Γ lim p e =  record {
-               TMap = λ i →  Sets [ proj i o ? ]
-             ; isNTrans = record { commute = ?  }
+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 Γ)) ) Γ
+SetsNat C I s  Γ  =  record {
+               TMap = λ i →  Sets [ proj i o e ]
+             ; isNTrans = record { commute = comm1 }
       } where
-    proj : ?
-    proj = ?
-    comm1 : ?
-    comm1 = ?
+    e  :  Hom Sets (slim  (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j))
+    e  =  λ x → record { pi1  = λ j →  slim-obj 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 )  )
+    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
+    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 ] ]
+    comm1 {a} {b} {f} = begin
+          Sets [ FMap Γ f o Sets [ proj a o e ]  ]
+        ≈⟨  extensionality Sets  ( λ x →  comm2 x )  ⟩
+          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 FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
+       ∎   where
+            open  ≈-Reasoning Sets
 
 
 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 = record { 
-               TMap = λ i →  Sets [ proj i o e ]  
-             ; isNTrans = record { commute = comm1 } 
-           }
+         ; t0 = SetsNat C I s Γ
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = {!!}
@@ -206,35 +226,7 @@
        }  where
           a0 : Obj Sets
           a0 =  slim  (ΓObj s Γ) (ΓMap s Γ) 
-          iid :  {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i)
-          iid {i} = FMap Γ ( small-iso s ) 
           e  :  Hom Sets a0 (iproduct I (λ j → ΓObj s Γ j))
           e  =  λ x → record { pi1  = λ j →  slim-obj x j }
-          proj :  (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
-          proj i prod = iid (  pi1 prod ( small→ s i )  )
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 = {!!}
-          comm2 :  {a b : Obj C} {f : Hom C a b} → ( x : a0 ) → (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
-          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 ] ]
-          comm1 {a} {b} {f} = begin
-                  Sets [ FMap Γ f o Sets [ proj a o e ]  ]
-              ≈⟨  extensionality Sets  ( λ x →  comm2 x )  ⟩
-                  Sets [ proj b o e ] 
-              ≈↑⟨ idR  ⟩
-                  Sets [ Sets [ proj b o e ] o id1 Sets a0 ]
-              ≈⟨⟩
-                  Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
-             ∎   where
-                  open  ≈-Reasoning Sets
-
-