Mercurial > hg > Members > kono > Proof > category

changeset 554:9e6aa4d77c3e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equ version on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Apr 2017 20:24:42 +0900
parents e33282817cb7
children 91d065bcfdc0
files SetsCompleteness.agda
diffstat 1 files changed, 47 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 08 15:07:56 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 09 20:24:42 2017 +0900
@@ -160,6 +160,12 @@
 
 open Small 
 
+≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C ) 
+    →  a  ≡  a'
+    →  b  ≡  b'
+    →  f a b  ≡  f a' b'
+≡cong2 _ refl refl = refl
+
 ΓObj :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
    (i : Obj C ) →　 Set c₁
 ΓObj s  Γ i = FObj Γ i
@@ -169,63 +175,81 @@
 Γ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 ) 
-       ( 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
+       snequ : { i j : OC } → ( f :  I → I ) →  sequ (sobj i) (sobj j) ( λ x → smap f ( snmap i ) ) (  λ x → snmap j )
 
 open snat
 
 open import HomReasoning
 open NTrans
-
 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 
+    → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) Γ
+Cone C I s  Γ  =  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 Γ) cequ )) f ] ]
+        Sets [ (λ sn →  (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) )) 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  )) ⟩
                  FMap Γ ( hom← s ( hom→ s f))  (snmap sn  a )
              ≡⟨⟩
                  ΓMap s Γ (hom→ s f) (snmap sn a ) 
-             ≡⟨ sncommute sn (hom→ s  f) ⟩
+             ≡⟨  fe=ge0 (snequ sn (hom→ s f))  ⟩
                  snmap sn 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 =  snat  (ΓObj s Γ) (ΓMap s Γ)  (elem ? refl )
-         ; t0 = Cone C I s Γ {!!}
+           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)  
+         ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  = limit1
              ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
              ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
+          snat-cong :    { snat tnat :  snat  (ΓObj s Γ) (ΓMap s Γ) }
+             → (( i : Obj C ) → snmap snat i ≡  snmap tnat i )
+             → ( ( i j : Obj C ) ( f : I → I ) →  ΓMap s Γ f ( snmap snat i )   ≡ snmap snat j )
+             → ( ( i j : Obj C ) ( f : I → I ) →  ΓMap s Γ f ( snmap tnat i )   ≡ snmap tnat j )
+             → snat ≡ tnat
+          snat-cong {s} {t}  eq1  eq2 eq3 =  begin
+             record { snmap = λ i →  snmap s i ; snequ = {!!}   }
+           ≡⟨ 
+            ≡cong2 ( λ x y →
+              record { snmap = λ i → x i  ; snequ = {!!} } )  (  extensionality Sets  ( λ  i  →  {!!} ) )
+                   ( extensionality Sets  ( λ  x  → 
+                   ( extensionality Sets  ( λ  i  → 
+                     ( extensionality Sets  ( λ  j  → 
+                       ( extensionality Sets  ( λ  f  →  {!!}
+                     ))))))))
+            ⟩
+               record { snmap = {!!} ; snequ = {!!} }
+            ≡⟨ {!!} ⟩
+               record { snmap = λ i →  snmap t i ; snequ  = {!!}  }
+                     ∎   where
+                          open  import  Relation.Binary.PropositionalEquality
+                          open ≡-Reasoning
           a0 : Obj Sets
-          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) (  λ {i j } → elem {!!} refl )
+          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
           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 { 
+          limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 
+          limit1 a t = λ ( x : a ) →  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 ]
+              ; snequ = λ {i} {j} f → elem (TMap t i x) (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
              ≡⟨⟩
@@ -233,18 +257,17 @@
              ∎  ) where
                   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 ]
+          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 ]
           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 →  ( TMap t i ) x ; snequ =   λ {i} {j} f → elem (TMap t i x) (comm2 t f )  }
+             ≡⟨ snat-cong {!!} {!!} {!!}  ⟩ 
+                  record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (f x)  }
              ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
-