Mercurial > hg > Members > kono > Proof > category

changeset 553:e33282817cb7

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 Sat, 08 Apr 2017 15:07:56 +0900
parents 09b1f66f7d7c
children 9e6aa4d77c3e
files SetsCompleteness.agda
diffstat 1 files changed, 19 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 08 11:35:51 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 08 15:07:56 2017 +0900
@@ -168,8 +168,9 @@
     {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( hom← s f ) 
 
-record snat  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j )
-     ( Equ : { i j :  OC  }  →  { f : I → I } →   sequ (sobj i) (sobj j) ( smap f ) ( smap (λ x → x ) )) :  Set   c₂  where
+record snat  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
+       ( snequ : { i j :  OC  }  →  sequ (sobj i) (sobj j) ( smap (λ x → x ) ) ( smap (λ x → x ) ) )
+      :  Set   c₂  where
    field 
        snmap : ( i : OC ) → sobj i 
        sncommute : { i j : OC } → ( f :  I → I ) →  smap f ( snmap i )  ≡ snmap j
@@ -179,15 +180,16 @@
 open import HomReasoning
 open NTrans
 
-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 (snat  (ΓObj s Γ) (ΓMap s Γ) {!!} ) ) Γ
-Cone C I s  Γ  =  record {
+Cone : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( s : Small C I )  ( Γ : Functor C (Sets  {c₁} ) )   
+      ( Cequ :  { i j : Obj C} → sequ (ΓObj s Γ i) (ΓObj s Γ j) ( ΓMap s Γ (λ x → x ) ) ( ΓMap s Γ (λ x → x ) )  )
+    → NTrans C Sets (K Sets C (snat  (ΓObj s Γ) (ΓMap s Γ) Cequ  ) ) Γ
+Cone C I s  Γ  cequ =  record {
                TMap = λ i →  λ sn →  snmap sn i 
              ; isNTrans = record { commute = comm1 }
       } where
     comm1 :  {a b : Obj C} {f : Hom C a b} →
         Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
-        Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) {!!} )) f ] ]
+        Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) cequ )) f ] ]
     comm1 {a} {b} {f} = extensionality Sets  ( λ  sn  →  begin
                  FMap Γ f  (snmap sn  a )
              ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn  a ))) (sym ( hom-iso s  )) ⟩
@@ -204,8 +206,8 @@
 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 =  snat  (ΓObj s Γ) (ΓMap s Γ)  {!!}
-         ; t0 = Cone C I s Γ
+           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)  (elem ? refl )
+         ; t0 = Cone C I s Γ {!!}
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
@@ -213,16 +215,17 @@
           }
        }  where
           a0 : Obj Sets
-          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) {!!} 
+          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) (  λ {i j } → elem {!!} refl )
           comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
           comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
-          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!} ) 
-          limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
-              sncommute = λ f → comm2 t f }
-          t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ]
+          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!}) 
+          limit1 a t = λ x →  record { 
+              snmap = λ i →  ( TMap t i ) x 
+              ; sncommute = λ f → comm2 t f }
+          t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ {!!}) i o limit1 a t ] ≈ TMap t i ]
           t0f=t {a} {t} {i} =  extensionality Sets  ( λ  x  →  begin
-                 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x
+                 ( Sets [ TMap (Cone C I s Γ {!!}) i o limit1 a t ]) x
              -- ≡⟨⟩
                  -- snmap ( record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f }  ) i
              ≡⟨⟩
@@ -231,13 +234,13 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
           limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ) {!!} )} →
-                ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
+                ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ {!!}) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
           limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
              ≡⟨ {!!} (ΓObj s Γ) (ΓMap s Γ) {!!}  {!!} {!!} ⟩
-                  record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
+                  record {  snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x
              ∎  ) where