Mercurial > hg > Members > kono > Proof > category

changeset 666:ba84fbc64c7d

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 15:21:20 +0900
parents 9904edf40547
children 60e881060534
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Oct 23 07:52:30 2017 +0900
+++ b/SetsCompleteness.agda	Mon Oct 23 15:21:20 2017 +0900
@@ -8,7 +8,7 @@
 open import Relation.Binary.Core
 open import Function
 import Relation.Binary.PropositionalEquality
--- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
+-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x )
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
 ≡cong = Relation.Binary.PropositionalEquality.cong
@@ -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 ) ⟩
+             ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets  ( λ  i  →  eq1 x i )) (eq5 x ( extensionality Sets ( λ i → eq1 x i ) )) ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = λ i j g → sncommute (f x ) i j g  }
              ≡⟨⟩
                   f x
@@ -264,13 +264,18 @@
                   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 : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≅ eq'
                   irr≅ refl refl = refl
                   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)
-                  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 = {!!}
+                  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)  )
+                      →  ( λ 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 = {!!}