Mercurial > hg > Members > kono > Proof > category

changeset 529:18aea9cb0fdb

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 Tue, 28 Mar 2017 21:36:03 +0900
parents 531547cf3b92
children 89af55191ec6
files SetsCompleteness.agda
diffstat 1 files changed, 11 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Tue Mar 28 18:18:38 2017 +0900
+++ b/SetsCompleteness.agda	Tue Mar 28 21:36:03 2017 +0900
@@ -194,13 +194,21 @@
           e  =  λ x → record { pi1  = λ j →  slim-obj x j }
           proj :  (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i
           proj i prod = iid (  pi1 prod ( small→ s i )  )
+          comm2 :  {a b : Obj C} {f : Hom C a b} → ( x : a0 ) → (Sets [ FMap Γ f o Sets [ proj a o e ] ]) x ≡ (Sets [ proj b o e ]) x 
+          comm2 {a} {b} {f} x =    begin
+                (FMap Γ f ) ( ( proj a o e )  x )
+             ≡⟨⟩
+                (FMap Γ f ) (  iid ( slim-obj x  (small→ s a) ))
+             ≡⟨ {!!}  ⟩
+                iid ( slim-obj x ( small→ s b )  ) 
+             ∎   where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
           comm1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈
                 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ]
           comm1 {a} {b} {f} = begin
                   Sets [ FMap Γ f o Sets [ proj a o e ]  ]
-              ≈⟨ assoc ⟩
-                  Sets [ Sets [ FMap Γ f o  proj a ] o e   ]
-              ≈⟨ {!!}  ⟩
+              ≈⟨  extensionality Sets  ( λ x →  comm2 x )  ⟩
                   Sets [ proj b o e ] 
               ≈↑⟨ idR  ⟩
                   Sets [ Sets [ proj b o e ] o id1 Sets a0 ]