Mercurial > hg > Members > kono > Proof > category
changeset 495:633df882db86
fryed1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Mar 2017 13:08:03 +0900 |
| parents | ba6a67523523 |
| children | 5c7908202d5a |
| files | cat-utility.agda freyd.agda freyd1.agda limit-to.agda pullback.agda |
| diffstat | 5 files changed, 38 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/cat-utility.agda Tue Mar 14 13:08:03 2017 +0900 @@ -308,7 +308,7 @@ limit : ( a : Obj A ) → ( t : NTrans I A ( K A I a ) Γ ) → Hom A a a0 t0f=t : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ∀ { i : Obj I } → A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] - limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → ( f : Hom A a a0 ) → ( ∀ { i : Obj I } → + limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K A I a ) Γ } → { f : Hom A a a0 } → ( ∀ { i : Obj I } → A [ A [ TMap t0 i o f ] ≈ TMap t i ] ) → A [ limit a t ≈ f ] record Limit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A )
--- a/freyd.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/freyd.agda Tue Mar 14 13:08:03 2017 +0900 @@ -82,9 +82,9 @@ e=id {e} uce=uc = let open ≈-Reasoning (A) in begin e - ≈↑⟨ limit-uniqueness (isLimit (lim F)) e ( λ {i} → uce=uc ) ⟩ + ≈↑⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → uce=uc ) ⟩ limit (isLimit (lim F)) a00 u - ≈⟨ limit-uniqueness (isLimit (lim F)) (id1 A a00) ( λ {i} → idR ) ⟩ + ≈⟨ limit-uniqueness (isLimit (lim F)) ( λ {i} → idR ) ⟩ id1 A a00 ∎ kfuc=uc : {c k1 : Obj A} → {p : Hom A k1 a00} → A [ A [ TMap u c o
--- a/freyd1.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/freyd1.agda Tue Mar 14 13:08:03 2017 +0900 @@ -166,10 +166,10 @@ TMap (limit-u comp (FIA Γ)) b o FMap (K A I (limit-c comp (FIA Γ))) f ∎ -gnat : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) - → ( glimit : LimitPreserve A I C G ) (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → +gnat : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) + → (a : CommaObj) → ( t : NTrans I CommaCategory (K CommaCategory I a) Γ ) → NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) -gnat {I} comp Γ glimit a t = record { +gnat {I} Γ a t = record { TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) ] ; isNTrans = record { commute = λ {x y f} → comm1 x y f } } where @@ -209,12 +209,24 @@ ≈ C [ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ] ] comm1 = let open ≈-Reasoning (C) in begin FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a - ≈⟨ {!!} ⟩ - limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) (gnat comp Γ glimit a t ) - ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) - (limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) - o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) - ) ( λ {i} → begin + ≈↑⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin + TMap (t0 (LimitC comp Γ glimit)) i o ( FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ) + ≈⟨ assoc ⟩ + ( TMap (t0 (LimitC comp Γ glimit)) i o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a + ≈⟨⟩ + ( FMap G ( TMap (limit-u comp (FIA Γ )) i ) o FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o hom a + ≈↑⟨ car ( distr G ) ⟩ + FMap G ( A [ TMap (limit-u comp (FIA Γ )) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) o hom a + ≈⟨ car ( fcong G ( t0f=t (isLimit (climit comp (FIA Γ ))))) ⟩ + FMap G (arrow (TMap t i)) o hom a + ≈⟨ comm ( TMap t i) ⟩ + hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) + ≈⟨⟩ + TMap (gnat Γ a t) i + ∎ + ) ⟩ + limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) (gnat Γ a t ) + ≈⟨ limit-uniqueness (isLimit (LimitC comp Γ glimit )) ( λ {i} → begin TMap (t0 (LimitC comp Γ glimit )) i o ( limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) @@ -235,8 +247,8 @@ FMap F ( A [ TMap (t0 ( climit comp (FIA Γ))) i o limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t) ] ) ≈⟨ cdr ( fcong F ( t0f=t (isLimit (climit comp (FIA Γ))))) ⟩ hom ( FObj Γ i ) o FMap F ( TMap (NIA Γ a t) i ) - ≈⟨ {!!} ⟩ - TMap {!!} i + ≈⟨⟩ + TMap (gnat Γ a t ) i ∎ ) ⟩ limit (isLimit (LimitC comp Γ glimit )) (FObj F ( limit-c comp (FIA Γ))) (tu comp Γ ) @@ -261,7 +273,7 @@ → CommaCategory [ comma-a0 comp Γ glimit a t ≈ f ] comma-uniqueness {I} comp Γ glimit a t f t=f = let open ≈-Reasoning (A) in begin limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) - ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) (arrow f) t=f ⟩ + ≈⟨ limit-uniqueness (isLimit ( climit comp (FIA Γ) ) ) t=f ⟩ arrow f ∎ @@ -275,6 +287,6 @@ isLimit = record { limit = λ a t → comma-a0 comp Γ glimit a t ; t0f=t = λ {a t i } → comma-t0f=t comp Γ glimit a t i ; - limit-uniqueness = λ {a} {t} f t=f → comma-uniqueness {I} comp Γ glimit a t f t=f + limit-uniqueness = λ {a} {t} {f} t=f → comma-uniqueness {I} comp Γ glimit a t f t=f } }
--- a/limit-to.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/limit-to.agda Tue Mar 14 13:08:03 2017 +0900 @@ -226,7 +226,7 @@ → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin k h fh=gh - ≈⟨ limit-uniqueness (isLimit lim) k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ + ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ k' ∎ @@ -290,7 +290,7 @@ ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ] ipu {i} q h = let open ≈-Reasoning A in refl-hom ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] - ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} h (ipu q h) + ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} (ipu q h) ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → (i : I ) → A [ qi i ≈ qi' i ] → A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ] @@ -309,4 +309,4 @@ ∎ ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] - ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i)) + ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))
--- a/pullback.agda Tue Mar 14 12:14:57 2017 +0900 +++ b/pullback.agda Tue Mar 14 13:08:03 2017 +0900 @@ -155,7 +155,7 @@ iso-l I Γ lim lim' o iso-r I Γ lim lim' ≈⟨⟩ limit (isLimit lim') (a0 lim) ( t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') - ≈↑⟨ limit-uniqueness (isLimit lim') ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim )(a0 lim') (t0 lim') )( λ {i} → ( begin + ≈↑⟨ limit-uniqueness (isLimit lim') ( λ {i} → ( begin TMap (t0 lim') i o ( limit (isLimit lim') (a0 lim) (t0 lim) o limit (isLimit lim) (a0 lim') (t0 lim') ) ≈⟨ assoc ⟩ ( TMap (t0 lim') i o limit (isLimit lim') (a0 lim) (t0 lim) ) o limit (isLimit lim) (a0 lim') (t0 lim') @@ -165,7 +165,7 @@ TMap (t0 lim') i ∎) ) ⟩ limit (isLimit lim') (a0 lim') (t0 lim') - ≈⟨ limit-uniqueness (isLimit lim') (id (a0 lim')) idR ⟩ + ≈⟨ limit-uniqueness (isLimit lim') idR ⟩ id (a0 lim' ) ∎ @@ -246,7 +246,7 @@ → A [ limit (isLimit (lim b )) a f ≈ g ] couniquness2 {b} {a} {f} {g} lim-g=f = let open ≈-Reasoning (A) in begin limit (isLimit (lim b )) a f - ≈⟨ limit-uniqueness (isLimit ( lim b )) g lim-g=f ⟩ + ≈⟨ limit-uniqueness (isLimit ( lim b )) lim-g=f ⟩ g ∎ @@ -266,7 +266,7 @@ isLimit = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; - limit-uniqueness = λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f + limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f } } where limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a (U Γ) @@ -362,7 +362,7 @@ isLimit = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; - limit-uniqueness = λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f + limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f } } where limit1 : (a : Obj A) → NTrans I A (K A I a) Γ → Hom A a lim @@ -437,7 +437,7 @@ isLimit = record { limit = λ a t → limit1 a t ; t0f=t = λ {a t i } → t0f=t1 {a} {t} {i} ; - limit-uniqueness = λ {a} {t} f t=f → limit-uniqueness1 {a} {t} {f} t=f + limit-uniqueness = λ {a} {t} {f} t=f → limit-uniqueness1 {a} {t} {f} t=f } } where ta = ta1 B Γ (a0 limitb) (t0 limitb) U @@ -509,7 +509,7 @@ limit1 a t ≈⟨⟩ FMap U (limit (isLimit limitb) (FObj F a) (tF a t )) o TMap η a - ≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb) (B [ TMap ε lim o FMap F f ] ) ( λ {i} → lemma1 i) )) ⟩ + ≈⟨ car ( fcong U (limit-uniqueness (isLimit limitb) ( λ {i} → lemma1 i) )) ⟩ FMap U ( B [ TMap ε lim o FMap F f ] ) o TMap η a -- Universal mapping ≈⟨ car (distr U ) ⟩ ( (FMap U (TMap ε lim)) o (FMap U ( FMap F f )) ) o TMap η a