Mercurial > hg > Members > kono > Proof > category
changeset 566:ecef5008cc17
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Apr 2017 11:04:14 +0900 |
| parents | 6cf91ef84ca0 |
| children | 9e727ce08b2c |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Apr 24 10:40:38 2017 +0900 +++ b/SetsCompleteness.agda Mon Apr 24 11:04:14 2017 +0900 @@ -246,9 +246,9 @@ snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f x ) } uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} → - ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (x : a ) - → elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t {!!} x ) ≡ snequ1 (f x ) {!!} - uniquness2 = {!!} + ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (f' : I → I ) → (x : a ) + → elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x ) ≡ snequ1 (f x ) f' + uniquness2 cif=t f' x = {!!} uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (Γ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 ] uniquness1 {a} {t} {f} cif=t = extensionality Sets ( λ x → begin @@ -260,7 +260,7 @@ extensionality Sets ( λ j → extensionality Sets ( λ f' → extensionality Sets ( λ x → - elm-cong ( elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x )) (snequ1 (f x) f' ) {!!} ) + elm-cong ( elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x )) (snequ1 (f x) f' ) ? ) ))) ) ⟩ record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }