Mercurial > hg > Members > kono > Proof > category

changeset 543:34f79fafbba4

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 Sat, 01 Apr 2017 15:18:14 +0900
parents bc3802c5c8e4
children 158aaded24b9
files SetsCompleteness.agda
diffstat 1 files changed, 18 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 31 17:44:53 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 01 15:18:14 2017 +0900
@@ -182,24 +182,24 @@
     →  f a b  ≡  f a' b'
 ≡cong2 _ refl refl = refl
 
-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 ) →
-     ( snmap s ≡ snmap t )  → s ≡ t
-snat-cong {c₂} {I} s t smt=sms =   begin
-                record { snmap = snmap s ; sncommute = λ f → sncommute s f }
-             -- ≡⟨  ≡cong2 ( λ sm ( sc : I → ? ≡ ?  ) → record { snmap = sm  ; sncommute = λ f → sc f }  ) smt=sms {!!} ⟩
-             ≡⟨ {!!} ⟩
-                record { snmap = snmap t ; sncommute = λ f → sncommute t f }
-             ∎   where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
+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 → record { snmap = λ i → x i ; sncommute =  λ {i} {j} f → {!!} } )  
+              ( extensionality Sets  ( λ  i  → eq1 i ) )
+              ( extensionality Sets  ( λ  i  → ( extensionality Sets  ( λ  j  → ( extensionality Sets  ( λ  f  → 
+                    irr1 i j f  {!!} {!!}))))))
+   where
+      irr1 : ( i j : OC ) ( f : I )  →  ( es et : SM f ( snmap s i )  ≡ snmap s j )  → es ≡ et 
+      irr1 i j f es et = {!!}
 
-snat1 :  { c₂ : Level }  { I OC :  Set  c₂ } { sobj :  OC →  Set  c₂ } 
-     { smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j } ( snmap0 : ( i : OC ) → sobj i )
-       { sncommute0 : { i j : OC } → ( f :  I ) →  smap f ( snmap0 i )  ≡ snmap0 j } 
-     → snat sobj smap
-snat1 snmap0 { sncommute0} = record { snmap = snmap0 ; sncommute = sncommute0 }
+
+-- ( extensionality Sets ( λ i → eq1 i ) ) {!!}
+--             (irr ( extensionality Sets ( λ i → ( extensionality Sets ( λ j → ( extensionality Sets ( λ f →  eq2 i j f ))))))
+--                  ( extensionality Sets ( λ i → ( extensionality Sets ( λ j → ( extensionality Sets ( λ f →  eq3 i j f )))))))
 
 open import HomReasoning
 open NTrans
@@ -261,9 +261,7 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
-             ≡⟨ snat-cong (  record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }  )  
-                       (record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }  ) 
-                        {!!}   ⟩
+             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) ?  {!!} {!!} ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x