Mercurial > hg > Members > kono > Proof > category
changeset 601:2e7b5a777984
prove fe=ge in limit-to
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Jun 2017 14:16:36 +0900 |
| parents | 3e2ef72d8d2f |
| children | b7659ad60a69 |
| files | SetsCompleteness.agda limit-to.agda |
| diffstat | 2 files changed, 39 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Sat Jun 03 09:46:59 2017 +0900 +++ b/SetsCompleteness.agda Mon Jun 05 14:16:36 2017 +0900 @@ -148,6 +148,31 @@ open ≡-Reasoning +-- +-- + -- + -- equ f + -- elem -------→ a ---------→ b + -- ^ . ---------→ + -- | . g + -- |k . + -- | . e + -- c + +-- +makeEqu : { c₂ : Level} → {a b c : Obj (Sets {c₂})} → (e : Hom (Sets {c₂}) c a ) → (f g : Hom (Sets {c₂}) a b) → IsEqualizer (Sets {c₂}) e f g +makeEqu {c₂} {a} {b} {c} e f g = record { + fe=ge = {!!} + ; k = λ {d} h eq → {!!} + ; ek=h = λ {d} {h} {eq} → {!!} + ; uniqueness = {!!} + } where + equ0 : IsEqualizer Sets (λ e → equ e )f g + equ0 = SetsIsEqualizer a b f g + c→equ0 : Hom Sets c ( sequ a b f g ) + c→equ0 = {!!} + + open Functor ----
--- a/limit-to.agda Sat Jun 03 09:46:59 2017 +0900 +++ b/limit-to.agda Mon Jun 05 14:16:36 2017 +0900 @@ -160,10 +160,9 @@ lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A TwoCat ) → {a b : Obj A} (f g : Hom A a b ) - → (fe=ge : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] ) → IsEqualizer A (equlimit A f g comp) f g -lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { - fe=ge = fe=ge +lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g = record { + fe=ge = fe=ge0 ; k = λ {d} h fh=gh → k {d} h fh=gh ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' @@ -180,6 +179,18 @@ lim = climit comp Γ inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ inat = IndexNat A f g + fe=ge0 : A [ A [ f o (equlimit A f g comp) ] ≈ A [ g o (equlimit A f g comp) ] ] + fe=ge0 = let open ≈-Reasoning A in begin + f o (equlimit A f g comp) + ≈⟨⟩ + FMap Γ arrow-f o TMap (limit-u comp Γ) discrete.t0 + ≈⟨ IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-f} ⟩ + TMap (limit-u comp Γ) discrete.t1 o FMap (K A (TwoCat {c₁} {c₂} )(limit-c comp Γ)) id-t0 + ≈↑⟨ IsNTrans.commute ( isNTrans ( limit-u comp Γ )) {discrete.t0} {discrete.t1} {arrow-g} ⟩ + FMap Γ arrow-g o TMap (limit-u comp Γ) discrete.t0 + ≈⟨⟩ + g o (equlimit A f g comp) + ∎ k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c k {d} h fh=gh = limit (isLimit lim) d (inat d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ]