Mercurial > hg > Members > kono > Proof > category

changeset 594:db76b73b526c

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 Mon, 22 May 2017 12:04:34 +0900
parents a158ebb391f2
children 0386e82f0dd8
files SetsCompleteness.agda
diffstat 1 files changed, 42 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun May 21 19:53:58 2017 +0900
+++ b/SetsCompleteness.agda	Mon May 22 12:04:34 2017 +0900
@@ -210,6 +210,35 @@
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
 
+≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C ) 
+    →  a  ≡  a'
+    →  b  ≡  b'
+    →  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 → I) →  SObj i → SObj j)  
+         { s t :  slim SObj SMap   }
+     → (( i : OC ) → slproj s i ≡  slproj t i )
+     → ( ( i j : OC ) ( f : I → I ) →  SMap {i} {j} f ( slproj s i )   ≡ slproj s j )
+     → ( ( i j : OC ) ( f : I → I ) →  SMap {i} {j} f ( slproj t i )   ≡ slproj t j )
+     → s ≡ t
+snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 =  begin
+     record { slproj = λ i →  slproj s i ; slequ  = λ i j f → slequ s i j f  }
+ ≡⟨ 
+    ≡cong2 ( λ x y →
+      record { slproj = λ i → x i  ; slequ  = λ i j f → {!!} } )  (  extensionality Sets  ( λ  i  →  eq1 i ) )
+           ( extensionality Sets  ( λ  x  → 
+           ( extensionality Sets  ( λ  i  → 
+             ( extensionality Sets  ( λ  j  → 
+               ( extensionality Sets  ( λ  f  → {!!} 
+             ))))))))
+  ⟩
+     record { slproj = λ i →  slproj t i ; slequ  = λ i j f → slequ t i j f  }
+             ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
+
 SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) ) 
     → Limit Sets C Γ
 SetsLimit { c₂} C I s Γ = record { 
@@ -223,17 +252,28 @@
        }  where
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ x →  record {
-               slequ =  λ i j f → elem {!!} ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ))
+               slequ =  λ i j f → elem i ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ))
                ; slproj =  λ i → ( TMap t i ) x
              }
           limit-uniqueness :  {a : Obj Sets} {t :  NTrans C Sets (K Sets C a) Γ}  {f : Hom Sets a (slim  (ΓObj s Γ) (ΓMap s Γ))} → ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ)  i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ]
           limit-uniqueness {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
                   limit1 a t x
-             ≡⟨ {!!} ⟩
+             ≡⟨⟩
+                  record { slproj = λ i →  TMap t i x  ; slequ =  λ i j f → elem i ( ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )) }
+             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩
+                  record { slproj = λ i →  slproj  (f x ) i  ; slequ = slequ (f x ) }
+             ≡⟨⟩
                   f x
              ∎  ) where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
+                  eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ slproj (f x) i
+                  eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
+                  eq2 : (x : a ) (i j : Obj C) (f : I → 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 → I) → ΓMap s Γ k (slproj (f x) i) ≡ slproj (f x) j
+                  eq3 x i j k =  fe=ge0 ( slequ (f x ) i j k )
+