Mercurial > hg > Members > kono > Proof > category

changeset 555:91d065bcfdc0

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 Sun, 09 Apr 2017 21:20:25 +0900
parents 9e6aa4d77c3e
children 6277ac99db37
files SetsCompleteness.agda
diffstat 1 files changed, 14 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Apr 09 20:24:42 2017 +0900
+++ b/SetsCompleteness.agda	Sun Apr 09 21:20:25 2017 +0900
@@ -109,6 +109,9 @@
 irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
 irr refl refl = refl
 
+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' )
+
 open sequ
 
 --           equalizer-c = sequ a b f g
@@ -129,8 +132,6 @@
            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
-           elm-cong :   (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' )
            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)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
            lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
@@ -216,28 +217,6 @@
              ; 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 Γ) 
           comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 
@@ -263,11 +242,21 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; snequ =   λ {i} {j} f → elem (TMap t i x) (comm2 t f )  }
-             ≡⟨ snat-cong {!!} {!!} {!!}  ⟩ 
+             ≡⟨ ≡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 (TMap t i x ) {!!}) ? {!!}
+                     ))))))))
+              ⟩ 
                   record {  snmap = λ i →  snmap  (f x ) i  ; snequ =  snequ (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  )
 
+