Mercurial > hg > Members > kono > Proof > category
changeset 572:46e417754601
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Apr 2017 22:26:59 +0900 |
| parents | 143de0e3eb60 |
| children | cc67ef472636 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 4 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Apr 24 21:08:57 2017 +0900 +++ b/SetsCompleteness.agda Mon Apr 24 22:26:59 2017 +0900 @@ -223,7 +223,7 @@ ≡⟨⟩ FMap Γ f (snmap (equ (slequ se (λ x → x))) a) ≡⟨ ≡cong ( λ g → FMap Γ g (snmap (equ (slequ se (λ x → x))) a)) (sym ( hom-iso s ) ) ⟩ - FMap Γ (hom← s ( hom→ s f)) (snmap (equ {_} {_} {_} {_} {_} (slequ se {a} {a} (λ x → x))) a) + FMap Γ (hom← s ( hom→ s f)) (snmap (equ (slequ se {a} {a} (λ x → x))) a) ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ ) ⟩ FMap Γ (hom← s ( hom→ s f)) (snmap (equ (slequ se (hom→ s f ))) a) ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ @@ -259,16 +259,15 @@ uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} → ( i j : Obj C ) → ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (f' : I → I ) → (x : a ) - → equ {_} {_} {slobj (f x) j } {{!!}} {{!!}} - (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t {i} {j} f' x)) ≡ equ (slequ (f x) f') + → record { snmap = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') uniquness2 {a} {t} {f} i j cif=t f' x = begin - record { snmap = λ i₁ → TMap t i₁ x } + record { snmap = λ i → TMap t i x } ≡⟨ ≡cong ( λ g → record { snmap = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ record { snmap = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x } ≡⟨⟩ record { snmap = λ i → snmap (equ (slequ (f x) {i} {i} (λ x → x )) ) i } ≡⟨ ≡cong ( λ g → record { snmap = λ i → g i } ) ( extensionality Sets ( λ i → lemma-equ C I s Γ )) ⟩ - record { snmap = λ i₁ → snmap (equ (slequ (f x) f')) i₁ } + record { snmap = λ i → snmap (equ (slequ (f x) f')) i } ∎ where open import Relation.Binary.PropositionalEquality open ≡-Reasoning