Mercurial > hg > Members > kono > Proof > category

changeset 548:03b851adc4fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 05 Apr 2017 22:04:38 +0900
parents c0078b03201c
children adef39d19884
files SetsCompleteness.agda
diffstat 1 files changed, 63 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Apr 04 13:51:48 2017 +0900
+++ b/SetsCompleteness.agda	Wed Apr 05 22:04:38 2017 +0900
@@ -176,9 +176,39 @@
 
 open snat
 
-snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) ( smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j )
-    ( snm : ( i : OC ) → sobj i ) →  (( snm1 : ( i : OC ) → sobj i ) ( i j :  OC  )  → (f : I ) → smap f ( snm1 i )  ≡ snm1 j ) → snat sobj smap
-snat1 SO SM snm eq = record { snmap = λ i → snm i ;   sncommute = λ {i} {j} f → eq snm i j f   }
+snmeq :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I )→  SO i → SO j }
+          ( s t :  snat SO SM  ) → ( i : OC ) → 
+         { snmapsi   snmapti : SO i } →  snmapsi ≡  snmapti → SO i
+snmeq s t i {pi} {.pi} refl   = pi
+
+snmc :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I )→  SO i → SO j }
+          ( s t :  snat SO SM  ) → { i j : OC } → { f :  I } →
+         { snmapsi   snmapti : SO i } →  (eqi : snmapsi ≡  snmapti ) → 
+         { snmapsj   snmaptj : SO j } →  (eqj : snmapsj ≡  snmaptj ) 
+         → ( SM f ( snmapsi )   ≡ snmapsj )
+         → ( SM f ( snmapti )   ≡ snmaptj ) 
+         → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj)
+snmc s t refl refl refl refl = refl
+
+snmc1 :  { c₂ : Level } { I OC :  Set  c₂ } { SO :  OC →  Set   c₂  } { SM : { i j :  OC  }  → (f : I )→  SO i → SO j }
+          ( s t :  snat SO SM  ) → { i j : OC } → { f :  I } →
+         { snmapsi   snmapti : SO i } →  (eqi : snmapsi ≡  snmapti ) → 
+         { snmapsj   snmaptj : SO j } →  (eqj : snmapsj ≡  snmaptj ) 
+         → ( SM f ( snmapsi )   ≡ snmapsj )
+         → ( SM f ( snmapti )   ≡ snmaptj ) → ( snm : (i : OC ) → SO i ) →
+            SM f (snm i) ≡ snm j
+snmc1 s t refl refl refl refl snm = {!!}
+
+snat1 :   { c₂ : Level }  { I OC :  Set  c₂ } ( SO :  OC →  Set  c₂ ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
+    →  ( s t :  snat SO SM   )
+    → ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) 
+     → ( eq2 : ( i j : OC ) ( f : I ) →  SM {i} {j} f ( snmap s i )   ≡ snmap s j )
+     → ( eq3 : ( i j : OC ) ( f : I ) →  SM {i} {j} f ( snmap t i )   ≡ snmap t j )
+    → snat SO SM
+snat1  SO SM s t eq1 eq2 eq3 =  record { 
+     snmap = λ i → snmeq s t i  (eq1 i ) ; 
+     sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f )
+   }
 
 ≡cong2 : { c : Level } { A B C : Set  c } { a a' : A } { b b' : B } ( f : A → B → C ) 
     →  a  ≡  a'
@@ -186,41 +216,34 @@
     →  f a b  ≡  f a' b'
 ≡cong2 _ refl refl = refl
 
+snmeqeqs  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
+          ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
+          snmeq s t i  (eq1 i )  ≡ snmap s i
+snmeqeqs SO SM s t i eq1  = lemma  (eq1 i) refl where
+    lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapsi  ≡ sm ) →
+          snmeq s t i  eq1  ≡ sm
+    lemma refl refl  = refl
+    
+snmeqeqt  : { c₂ : Level } { I OC :  Set  c₂ } ( SO :  OC →  Set   c₂  ) ( SM : { i j :  OC  }  → (f : I )→  SO i → SO j )
+          ( s t :  snat SO SM  ) → ( i : OC ) →  ( eq1 : ( i : OC ) → snmap s i ≡  snmap t i ) →
+          snmeq s t i  (eq1 i )  ≡ snmap t i
+snmeqeqt SO SM s t i eq1  = lemma  (eq1 i) refl where
+    lemma  :  { snmapsi   snmapti sm : SO i } → ( eq1 : snmapsi ≡  snmapti ) → ( snmapti  ≡ sm ) →
+          snmeq s t i  eq1  ≡ sm
+    lemma refl refl  = refl
+
+-- irr2 : { c₂ : Level}  {d : Set c₂ }  { x1 x2 y1 y2  : d } ( eqx :  x1  ≡ x2 )( eqy :  y1  ≡ y2 ) 
+--     ( eq1 :  x1  ≡ y1 ) ( eq2 :  x2  ≡ y2 ) →  eq1 ≡  eq2
+-- irr2 = ?
+
 snat-cong :  { c : Level }  { I OC :  Set  c }  ( SObj :  OC →  Set  c  ) ( SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j)  
          { s t :  snat SObj SMap   }
      → (( i : OC ) → snmap s i ≡  snmap t i )
      → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap s i )   ≡ snmap s j )
      → ( ( i j : OC ) ( f : I ) →  SMap {i} {j} f ( snmap t i )   ≡ snmap t j )
      → s ≡ t
-snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  ≡cong2 ( λ x y → snat1 SO SM x y ) 
-              ( extensionality Sets  ( λ  i  → eq1 i ) )
-              ( extensionality Sets  ( λ  snm  → 
-                 ( extensionality Sets  ( λ  i  →  
-                 ( extensionality Sets  ( λ  j  →  
-                 ( extensionality Sets  ( λ  f  →   irr2 snm i j f ( eq2s i j f (eq1 i)  snm (eq2 i j f ) ) {!!} ))))))))
-   where
-      eq2s1 : { i j : OC } { f : I }  →  {si : SO i} { sj : SO j } 
-           ( snm : ( i : OC ) → SO i ) → ( si ≡  snm i ) → ( sj ≡  snm j ) → SM {i} {j} f  si ≡ sj →  SM f ( snm i) ≡ snm j
-      eq2s1 {i} {j} {f} {si} {sj}  snm eq1 eq2 eq3 =  begin
-                 SM f ( snm i)  
-             ≡⟨ ≡cong (λ x → SM f x ) (sym eq1)  ⟩
-                 SM f si  
-             ≡⟨ eq3 ⟩
-                 sj  
-             ≡⟨ eq2 ⟩
-                snm j
-             ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
-      eq2s : ( i j : OC ) ( f : I )  →   ( snmap s i ≡  snmap t i ) → 
-           ( snm : ( i : OC ) → SO i ) → SM {i} {j} f ( snmap s i )   ≡ snmap s j →  SM f ( snm i) ≡ snm j
-      eq2s i j f eq1 snm eq2 =  eq2s1 snm {!!} {!!} eq2
-      irr3 : { i j : OC } { f : I }  →  {snmapsi :  SO i  }  → {snmapsj :  SO j  } →
-           ( es et : SM f ( snmapsi )  ≡ snmapsj  )  → es  ≡ et
-      irr3 refl refl = refl
-      irr2 :  ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I )  →  
-              ( es et : SM f (snm i )  ≡ snm j ) →  es  ≡ et 
-      irr2 snm i j f  es et = irr3 es et 
+snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 = ≡cong2 ( λ x y →
+     record { snmap = λ i → x i  ; sncommute  = y x } )  (extensionality Sets  ( λ  i  →  eq1 i  ))  {!!}
 
 
 open import HomReasoning
@@ -283,13 +306,19 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
-             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) {!!}  {!!} {!!} ⟩
+             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (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 : (x : a ) (i j : Obj C) (f : I) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
+                  eq2 x i j f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
+                  eq3 :  (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j
+                  eq3 x i j k =  sncommute (f x )  k
 
 
 
@@ -299,3 +328,4 @@
 
 
 
+