Mercurial > hg > Members > kono > Proof > category

changeset 665:9904edf40547

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Oct 2017 07:52:30 +0900
parents 9e8276b89cd0
children ba84fbc64c7d
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Oct 22 23:36:30 2017 +0900
+++ b/SetsCompleteness.agda	Mon Oct 23 07:52:30 2017 +0900
@@ -251,7 +251,7 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ i j f → comm2 t f }
-             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq2 x ) ⟩
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq5 x ) ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j g → sncommute (f x ) i j g  }
              ≡⟨⟩
                   f x
@@ -260,12 +260,17 @@
                   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) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x -- hg cat -r 550 SetsCompleteness.agda
+                  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 ) i j k
                   irr≅ : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≅ eq'
                   irr≅ refl refl = refl
-                  eq3 :  ( x : a)  ( i j : Obj C ) ( g : I ) → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g }  )
-                      ≅  sncommute (f x) i j g
-                  eq3 x i j g = {!!}
+                  eq4 :  ( x : a)  ( i j : Obj C ) ( g : I )
+                     → TMap t i x ≡ snmap (f x) i
+                     → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g }  ) ≅  sncommute (f x) i j g
+                  eq4 x i j g eq = {!!} -- irr≅ ? ?
                   -- eq2 :  ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x)
-                  eq2 :  ( x : a) →  ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ))
+                  eq5 :  ( x : a) →  ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ))
                       ≅ ( λ i j g →  sncommute (f x) i j g )
-                  eq2 x = {!!}
+                  eq5 x = {!!}