Mercurial > hg > Members > kono > Proof > category
changeset 513:e73c3e73a87b
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 21 Mar 2017 09:38:57 +0900 |
| parents | f19dab948e39 |
| children | 1fca61019bdf |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 10 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Mar 20 12:50:21 2017 +0900 +++ b/SetsCompleteness.agda Tue Mar 21 09:38:57 2017 +0900 @@ -122,14 +122,22 @@ ek=h {d} {h} {eq} = refl fhy=ghy : (d : Obj Sets ) ( h : Hom Sets d a ) (y : d ) → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]) → f (h y) ≡ g (h y) fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh + fuga : {d : Obj Sets} { y : d } { k' : Hom Sets d (sequ a b f g)} → Hom Sets a {!!} + fuga = {!!} repl : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → ( y : d ) → Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y repl {d} {h} {fh=gh} {k'} y ek'=h = begin k h fh=gh y ≡⟨⟩ - elem (h y) (fhy=ghy d h y fh=gh ) - ≡⟨ ? ⟩ + elem (h y) (fhy=ghy d h y fh=gh ) + ≡⟨ {!!} ⟩ + fuga (h y ) + ≡⟨ sym ( Category.cong (λ f → fuga (f y ) ) ek'=h ) ⟩ + fuga ( ( λ e → equ e ) ( k' y ) ) + ≡⟨⟩ + ( λ e → fuga ( equ e )) ( k' y ) + ≡⟨ {!!} ⟩ k' y ∎ where