Mercurial > hg > Members > kono > Proof > category
changeset 588:11b5eeb4a9e7
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 May 2017 13:45:31 +0900 |
| parents | d3bea3ac919e |
| children | 6584db867bd0 |
| files | SetsCompleteness.agda |
| diffstat | 1 files changed, 7 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Fri May 12 10:25:05 2017 +0900 +++ b/SetsCompleteness.agda Fri May 12 13:45:31 2017 +0900 @@ -232,5 +232,11 @@ -- sequ (Obj C) (ΓObj s Γ j) (λ x₁ → ΓMap s Γ f (proj (e x₁) i)) (λ x₁ → proj (e x₁) j) limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) limit1 a t = λ x → record { slequ = λ i j f → k (λ p → - iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) (extensionality Sets ( λ y → ? )) x + iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) ( begin + (λ x₁ → ΓMap s Γ f (proj x₁ i)) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) + ≈⟨ car (nat t) ⟩ + (λ x₁ → proj x₁ j) o (λ p → iproduct1 (Obj C) (ΓObj s Γ) (TMap t) x) + ∎ + ) x ; slprod = record { proj = λ i → TMap t i x } } + where open ≈-Reasoning (Sets { c₂})