Mercurial > hg > Members > kono > Proof > category
changeset 614:e6be03d94284
Representational Functor preserve limit done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 13 Jun 2017 22:53:44 +0900 |
| parents | afddfebea797 |
| children | a45c32ceca97 |
| files | freyd2.agda |
| diffstat | 1 files changed, 15 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd2.agda Tue Jun 13 22:36:54 2017 +0900 +++ b/freyd2.agda Tue Jun 13 22:53:44 2017 +0900 @@ -120,7 +120,7 @@ UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i - ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!} + ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t } where hat0 : NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ) hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b) @@ -163,6 +163,20 @@ ≈⟨⟩ TMap t i x ∎ )) + limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)} {f : Hom Sets a (FObj (HomA A b) (a0 lim))} → + ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o f ] ≈ TMap t i ]) → + Sets [ ψ a t ≈ f ] + limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin + ψ a t x + ≈⟨⟩ + FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) + ≈⟨⟩ + limit (isLimit lim) b (ta a x t ) o id1 A b + ≈⟨ idR ⟩ + limit (isLimit lim) b (ta a x t ) + ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ + f x + ∎ )) UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ)