Mercurial > hg > Members > kono > Proof > category
changeset 571:143de0e3eb60
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Apr 2017 21:08:57 +0900 |
| parents | 3d6d8fea3e09 |
| children | 46e417754601 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 5 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Apr 24 20:44:21 2017 +0900 +++ b/SetsCompleteness.agda Mon Apr 24 21:08:57 2017 +0900 @@ -210,7 +210,6 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning - Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ Cone C I s Γ = record { @@ -224,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 ) ) ⟩ @@ -260,7 +259,8 @@ 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 (elem (record { snmap = λ i₁ → TMap t i₁ x }) (limit2 a t {i} {j} f' x)) ≡ equ (slequ (f x) f') + → 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') uniquness2 {a} {t} {f} i j cif=t f' x = begin record { snmap = λ i₁ → TMap t i₁ x } ≡⟨ ≡cong ( λ g → record { snmap = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ @@ -277,13 +277,13 @@ uniquness1 {a} {t} {f} cif=t = extensionality Sets ( λ x → begin limit1 a t x ≡⟨⟩ - record { slequ = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f x ) } + record { slequ = λ {i} {j} f' → elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x ) } ≡⟨ ≡cong ( λ e → record { slequ = λ {i} {j} f' → e i j f' x } ) ( extensionality Sets ( λ i → extensionality Sets ( λ j → extensionality Sets ( λ f' → extensionality Sets ( λ x → - elm-cong ( elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 i j cif=t f' x ) ) + elm-cong ( elem ( record { snmap = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) ) ))) ) ⟩ record { slequ = λ {i} {j} f' → slequ (f x ) f' }