Mercurial > hg > Members > kono > Proof > category

changeset 530:89af55191ec6

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:10:52 +0900
parents 18aea9cb0fdb
children 66cad3cb3a66
files SetsCompleteness.agda
diffstat 1 files changed, 21 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 28 21:36:03 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 22:10:52 2017 +0900
@@ -169,9 +169,27 @@
      ( 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
 
 open slim
 
+open import HomReasoning
+
+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 = ?  }
+      } where
+    proj : ?
+    proj = ?
+    comm1 : ?
+    comm1 = ?
+
+
 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 { 
@@ -181,7 +199,7 @@
              ; isNTrans = record { commute = comm1 } 
            }
          ; isLimit = record {
-               limit  = {!!}
+               limit  = limit1
              ; t0f=t = {!!}
              ; limit-uniqueness  = {!!}
            }
@@ -194,6 +212,8 @@
           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 )
@@ -215,7 +235,6 @@
               ≈⟨⟩
                   Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] 
              ∎   where
-                  open import HomReasoning
                   open  ≈-Reasoning Sets