Mercurial > hg > Members > kono > Proof > category

changeset 668:07c84c8d9e4f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
SetCompleteness done!
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Oct 2017 11:57:49 +0900
parents 60e881060534
children 220ea177572f
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Oct 27 10:01:35 2017 +0900
+++ b/SetsCompleteness.agda	Mon Oct 30 11:57:49 2017 +0900
@@ -182,7 +182,7 @@
 ≡cong2 _ refl refl = refl
 
 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
-    using (_≅_;refl)
+    using (_≅_;refl; ≡-to-≅)
 postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂
 
 snat-cong : {c : Level}
@@ -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 )) (eq5 x ( extensionality Sets ( λ i → eq1 x i ) )) ⟩
+             ≡⟨ 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
@@ -264,17 +264,16 @@
                   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
-                  eq3' : (x : a ) (i j : Obj C) (k : I) → 
-                      ( ΓMap s Γ k (TMap t i x) ≡ TMap t j x ) ≡ ( ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j )  
-                  eq3' x i j k = ≡cong ( λ h →  ( ΓMap s Γ k (h i) ≡ h j ))  ( extensionality Sets ( λ i → eq1 x i ) )
-                  irr≅ : { c₂ : Level}  {d e : Set c₂ }  { x : d } { y : e } ( ee :  d  ≡ e )  ( eq eq' :  x  ≅ y ) → eq ≅ eq'
-                  irr≅ refl refl refl = refl
+                  irr≅ : { c₂ : Level}  {d e : Set c₂ }  { x1 y1 : d } { x2 y2 : e }
+                      ( ee :  x1 ≅ x2 ) ( ee :  y1  ≅ y2 )  ( eq :  x1  ≡ y1 ) ( eq' :  x2  ≡ y2 ) → eq ≅ eq'
+                  irr≅ refl refl refl refl = refl
                   eq4 :  ( 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
-                  eq4 x i j g = ? -- irr≅ ? ? ?
-                  postulate eq6 : {a : Level } {A : Set a} {B : A → Set a} {f g : (y : A) → B y} → (∀ y → f y ≡ g y) → ( ( λ y → f y ) ≅ ( λ y → g y ))
-                  -- eq5 :  ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x)
-                  eq5 :  ( x : a) → ( ( λ i → TMap t i x ) ≡ snmap (f x)  )
+                  eq4 x i j g = irr≅ (≡-to-≅ (≡cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g )
+                  -- heterogenous extensionarity
+                  postulate eq6 : {a : Level } {A : Set a} {B B' : A → Set a}
+                               {f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y ))
+                  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 )
-                  eq5 x eq = {!!} 
+                  eq5 x = eq6 ( λ i → eq6 ( λ j → eq6 ( λ g → eq4 x i j g ) ) )