Mercurial > hg > Members > kono > Proof > category

changeset 562:14483d9d604c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end again ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 10 Apr 2017 12:16:01 +0900
parents 2c0e168c832e
children 8b18361e6ca9
files SetsCompleteness.agda
diffstat 1 files changed, 24 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Apr 10 10:48:50 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 10 12:16:01 2017 +0900
@@ -187,7 +187,8 @@
 record snequ  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
       :  Set   c₂  where
    field 
-       snequ1 : { i j : OC } → ( f :  I → I ) →  sequ ( snproj sobj smap ) (sobj j) ( λ x → smap f ( snmap x i ) ) (  λ x → snmap x j )
+       sn :  snproj sobj smap
+       snequ1 : { i j : OC } → ( f :  I → I ) →  sequ (sobj i) (sobj j) ( λ x → smap f ( snmap sn i ) ) (  λ x → snmap sn j )
 
 open snequ
 
@@ -197,24 +198,21 @@
 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 (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ
 Cone C I s  Γ =  record {
-               TMap = λ i →  λ se → snmap ( equ ( snequ1 se {i} {i} (λ x → x )) ) i
+               TMap = λ i →  λ se → snmap ( sn se ) i
              ; isNTrans = record { commute = comm1 }
       } where
     comm1 :  {a b : Obj C} {f : Hom C a b} →
-        Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (snequ1 se (λ x → x))) a) ] ≈
-        Sets [ (λ se → snmap (equ (snequ1 se (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
-    comm1 {a} {b} {f} = begin
-                FMap Γ f o (λ se → snmap (equ (snequ1 se (λ x → x))) a)
-             ≈⟨⟩
-                ( λ se → FMap Γ f (snmap se a ))  o   (λ se → equ (snequ1 se (λ x → x)) )
-             ≈⟨   {!!}  ⟩
-                ( λ se → snmap se b  ) o   (λ se → equ (snequ1 se (λ x → x)) )
-             ≈⟨⟩
-                (( λ se → snmap se b  ) o   (λ se → equ (snequ1 se (λ x → x)) ) )  o id1 Sets ( snequ (ΓObj s Γ) (ΓMap s Γ)  )
-             ≈⟨⟩
-                (λ se → snmap (equ (snequ1 se (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f
-             ∎  where
-                  open  ≈-Reasoning Sets
+        Sets [ Sets [ FMap Γ f o (λ se → snmap (sn se) a) ] ≈
+        Sets [ (λ se → snmap (sn se) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
+    comm1 {a} {b} {f} =   extensionality Sets  ( λ  se  →  begin  
+                  FMap Γ f (snmap (sn se) a)
+             ≡⟨ ≡cong ( λ f → FMap Γ f ( snmap (sn se) a )) (sym ( hom-iso s ))  ⟩
+                  FMap Γ (hom← s ( hom→ s f)) (snmap (sn se) a)
+             ≡⟨ fe=ge0 ( snequ1 se (hom→ s f ) )  ⟩
+                  snmap (sn se) 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 Γ
@@ -227,19 +225,15 @@
              ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
           }
        }  where
-          a0 : Obj Sets
-          a0 =  snequ  (ΓObj s Γ) (ΓMap s Γ) 
           setprod : {a : Obj Sets} → NTrans C Sets (K Sets C a) Γ → (x : a ) → snproj  (ΓObj s Γ) (ΓMap s Γ)
           setprod t x  = record { snmap = λ i → TMap t i x }
-          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 ) )
           comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
-              → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap x₁ i)) o setprod t ] ≈ Sets [ (λ x₁ → snmap x₁ j) o setprod t ] ]
-          comm3 {a} {x} t f =  IsNTrans.commute (isNTrans t )
+              →  Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap (setprod t x) i)) o TMap t i ] ≈ Sets [ (λ x₁ → snmap (setprod t x) j) o TMap t i ] ]
+          comm3 {a} {x} t f =   {!!}
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ ( x : a ) →  record {
-                snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x
+                sn =  setprod t x
+                ; snequ1 = λ {i} {j} f → k (TMap t i ) (comm3 t f ) x 
             }
           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
@@ -254,40 +248,16 @@
           limit-uniqueness {a} {t} {f} cif=t = extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
              ≡⟨⟩
-                  record { snequ1 = λ {i} {j} f' → k ( setprod t ) (comm3 {a} {x} t f' ) x }
-             ≡⟨ ≡cong ( λ ff → record { snequ1 = λ {i} {j} f' → ff i j f' }) (  
-                            extensionality Sets  ( λ  i  →  extensionality Sets  ( λ  j  →  extensionality Sets  ( λ  f'  
-                                → k-cong {i} {j} f' x 
-                            )))
-                      ) ⟩
-                  record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' }
+                  record { sn =  setprod t x  ; snequ1 = λ {i} f' → k ( TMap t i ) (comm3 {a} {x} t f' ) x }
+             ≡⟨ ≡cong2 {!!} {!!} {!!}  ⟩
+                  record { sn = sn ( f x ) ; snequ1 = λ {i} {j} f' →  ( snequ1 (f x ) f' )  }
              ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
                   snmap-cong : ( e : snequ  (ΓObj s Γ) (ΓMap s Γ) ) {i : Obj C } { f g : I → I } 
-                        →   snmap ( equ ( snequ1 e  f)) i ≡  snmap ( equ ( snequ1 e  g)) i
+                        →   {!!} -- snmap ( equ ( snequ1 e  f)) i ≡  snmap ( equ ( snequ1 e  g)) i
                   snmap-cong e {i} =  ≡cong ( λ s → snmap s i ) refl
-                  k-cong : { i j : Obj C } ( f' : I → I )  ( x : a ) →   k ( setprod t ) (comm3 {a} {x} t f' ) x ≡  snequ1 (f x) f' 
-                  k-cong {i} {j} f' x = begin 
-                            k ( setprod t ) (comm3 {a} {x} t f' ) x
-                        ≡⟨ elm-cong (k ( setprod t ) (comm3 {a} {x} t f' ) x ) ( snequ1 (f x) f' )  ( begin 
-                               equ (k (setprod t) (comm3 {a} {x} t f') x)
-                            ≡⟨⟩
-                               record { snmap =  λ i' → TMap t i' x }
-                            ≡⟨ ≡cong ( λ s → record { snmap = λ i' → s i' } ) ( extensionality Sets  ( λ  i'  → ( sym ( begin
-                                    snmap ( equ ( snequ1 (f x) f')) i'
-                                  ≡⟨ snmap-cong (f x) ⟩
-                                    snmap ( equ ( snequ1 (f x) (λ x → x ))) i'
-                                  ≡⟨  ≡cong ( λ f → f x ) cif=t   ⟩
-                                     TMap t i' x
-                               ∎ )))) ⟩
-                               record { snmap =  λ i' → snmap (equ (snequ1 (f x) f')) i' }
-                            ≡⟨⟩
-                               equ (snequ1 (f x) f')
-                            ∎  
-                     ) ⟩
-                            snequ1 (f x) f'
-                     ∎  
-
+                  k-cong : { i j : Obj C } ( f' : I → I )  ( x : a ) →   k ( TMap t i ) {!!} x ≡  snequ1 (f x) f' 
+                  k-cong {i} {j} f' x =  {!!}