Mercurial > hg > Members > kono > Proof > category

changeset 998:98f412058488

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 Sun, 07 Mar 2021 15:57:49 +0900
parents d9419216ae0c
children d89f2c8cf0f4
files src/SetsCompleteness.agda
diffstat 1 files changed, 4 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/SetsCompleteness.agda	Sun Mar 07 15:51:45 2021 +0900
+++ b/src/SetsCompleteness.agda	Sun Mar 07 15:57:49 2021 +0900
@@ -219,15 +219,11 @@
           ee : Hom Sets (sequ a b f g)  a
           ee (elem y eq) = y
           k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d
-          k {d} h hf=hg ec = {!!} where
+          k {d} h hf=hg = cd where
+             ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a  -- (λ x → h (f x)) ≡ (λ x → h (g x))
+             ca eq = {!!}
              cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
-             cd ec = h ( f {!!} ) 
-             ff : sequ a b f g → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
-             ff (elem x eq) = elem x (cong (λ k → k x ) hf=hg )
-             gg : {y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ])  
-             gg {y} eq  = ff (ec eq)
-             hoge : ({y : a} → f y ≡ g y → sequ a d ( Sets [ h o f ]) (Sets [ h o g ]) ) → d
-             hoge ed = {!!}
+             cd = {!!}
           ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] }
            →   Sets [ Sets [ k h eq o equc f g ] ≈ h ]
           ke=h {d} {h} {eq} =  extensionality Sets  ( λ  x → begin