Mercurial > hg > Members > kono > Proof > category
changeset 567:9e727ce08b2c
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Apr 2017 11:48:35 +0900 |
| parents | ecef5008cc17 |
| children | f3fb9061a8ca |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 3 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Apr 24 11:04:14 2017 +0900 +++ b/SetsCompleteness.agda Mon Apr 24 11:48:35 2017 +0900 @@ -247,8 +247,8 @@ } 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 ]) → (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 = {!!} + → equ (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t f' x)) ≡ equ (snequ1 (f x) f') + uniquness2 cif=t f' x = refl 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' ) (uniquness2 cif=t f' x ) ) ))) ) ⟩ record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }