Mercurial > hg > Members > kono > Proof > category

changeset 558:c2eb1a2570ce

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 Mon, 10 Apr 2017 02:10:37 +0900
parents 9902722e1578
children e8ab4fcfe033
files SetsCompleteness.agda
diffstat 1 files changed, 56 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Apr 09 22:58:50 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 10 02:10:37 2017 +0900
@@ -112,6 +112,14 @@
 elm-cong :  {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →   (x y : sequ a b f g) → equ x ≡ equ y →  x  ≡ y
 elm-cong ( elem x eq  ) (elem .x eq' ) refl   =  ≡cong ( λ ee → elem x ee ) ( irr eq eq' )
 
+fe=ge  : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
+fe=ge  =  extensionality Sets (fe=ge0 ) 
+k : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} (h : Hom Sets d a) 
+     → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
+k {_} {_} {_} {_} {_} {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
+ek=h : {  c₂ : Level}  →  {a b : Obj (Sets {c₂}) }  {f g : Hom (Sets {c₂}) a b} →  {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
+ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = refl 
+
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -121,15 +129,9 @@
 SetsIsEqualizer {c₂} a b f g = record { 
                fe=ge  = fe=ge
              ; k = k
-             ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
+             ; ek=h = λ {d} {h} {eq} → ek=h {c₂} {a} {b} {f} {g} {d} {h} {eq}
              ; uniqueness  = uniqueness
        } where
-           fe=ge  :  Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
-           fe=ge  =  extensionality Sets (fe=ge0 ) 
-           k :  {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g)
-           k {d} h eq = λ x → elem  (h x) ( ≡cong ( λ y → y x ) eq )
-           ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e )  o k h eq ] ≈ h ]
-           ek=h {d} {h} {eq} = refl 
            injection :  { c₂ : Level  } {a b  : Obj (Sets { c₂})} (f  : Hom Sets a b) → Set c₂
            injection f =  ∀ x y  → f x ≡ f y →  x  ≡ y
            lemma5 :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
@@ -175,41 +177,49 @@
     {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 ) 
+record snproj  { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) 
       :  Set   c₂  where
    field 
        snmap : ( i : OC ) → sobj i 
-       snequ : { i j : OC } → ( f :  I → I ) →  sequ (sobj i) (sobj j) ( λ x → smap f ( snmap i ) ) (  λ x → snmap j )
+
+open snproj
 
-open snat
+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 )
+
+open snequ
+
 
 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 {
-               TMap = λ i →  λ sn → snmap sn i
+    → 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
              ; 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 ] ]
-    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 ) 
-             ≡⟨  fe=ge0 (snequ sn (hom→ s f))  ⟩
-                 snmap sn b
-             ∎  ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+        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
 
 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 Γ)  
+           a0 =  snequ  (ΓObj s Γ) (ΓMap s Γ)  
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
                limit  = limit1
@@ -218,14 +228,14 @@
           }
        }  where
           a0 : Obj Sets
-          a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
+          a0 =  snequ  (Γ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 : a ) →  record { 
-              snmap = λ i →  ( TMap t i ) x 
-              ; snequ = λ {i} {j} f → elem (TMap t i x) (comm2 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 → elem ( record { snmap = λ i → 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
@@ -236,29 +246,28 @@
              ∎  ) 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 Γ) )} →
+          limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (Γ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 ; snequ =   λ {i} {j} f → elem (TMap t i x) (comm2 t f )  }
-             ≡⟨ ≡cong2 ( λ x y →   record { snmap = λ i → x i  ; snequ = λ {i} {j} f → y x i j f }   ) 
-                 ( extensionality Sets  ( λ  i →   eq1  x i ) )
-                   ( extensionality Sets  ( λ  x'  → 
-                   ( extensionality Sets  ( λ  i  → 
-                     ( extensionality Sets  ( λ  j  → 
-                       ( extensionality Sets  ( λ  f'  → elm-cong (elem (x' i ) {!!} ) {!!}  (   eq1  x i   )
-                     ))))))))
-              ⟩ 
-                  record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (f x)  }
+                  record {  snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( comm2 t f ) }
+             ≡⟨ ≡cong ( λ se → record { snequ1 = λ {i} {j} f → se i j f  }) 
+                  (  extensionality Sets  ( λ  i  →  ( extensionality Sets  ( λ  j  →  ( extensionality Sets  ( λ  f'  → 
+                      sncong x f' i  {!!} (  ≡cong ( λ f → f x ) cif=t    )
+                  ))))))
+               ⟩
+                  record {  snequ1 =  snequ1 (f x)  }
              ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
-                  eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
-                  eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
-                  eq2 : ( i j : Obj C ) (x' : Obj C → FObj Γ {!!} )   → (f' : I → I )  →   ΓMap s Γ f' (x' i) ≡ x' j
-                  eq2 = {!!}
+                  sncong :  (x : a) → (f' : I → I ) → ( i : Obj C ) → ( se : snequ (ΓObj s Γ) (ΓMap s Γ) ) 
+                       →  snmap ( equ ( snequ1 se {i} {i} (λ x → x )) ) i  ≡  TMap t i x
+                       → elem (record { snmap = λ i → TMap t i x }) (comm2 t f') ≡ snequ1 (f x) f'
+                  sncong x f' i se eq = {!!}
 
 
+
+