Mercurial > hg > Members > kono > Proof > category
changeset 493:de9ce7e0d97c
on going using limit-uniquness directly
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 14 Mar 2017 11:43:46 +0900 |
| parents | c7b8017bcd4d |
| children | ba6a67523523 |
| files | freyd1.agda |
| diffstat | 1 files changed, 65 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/freyd1.agda Mon Mar 13 13:22:40 2017 +0900 +++ b/freyd1.agda Tue Mar 14 11:43:46 2017 +0900 @@ -19,10 +19,19 @@ open Limit open IsLimit +-- +-- -- F : A → C -- G : A → C -- +-- if A is complete and G preserve limit, Comma Category F↓G is complete +-- i.e. it has limit for Γ : I → F↓G +-- +-- +-- +--- Get a functor Functor I A from a functor I CommaCategory +--- FIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) → Functor I A FIA {I} Γ = record { FObj = λ x → obj (FObj Γ x ) ; @@ -39,6 +48,18 @@ id1 A (obj (FObj Γ x)) ∎ +Γa : { I : Category c₁ c₂ ℓ } → ( a : Obj A) → Functor I A +Γa a = record { + FObj = λ x → a ; + FMap = λ {x} {y} f → id1 A a ; + isFunctor = record { + identity = let open ≈-Reasoning (A) in refl-hom + ; distr = let open ≈-Reasoning (A) in sym ( idL ) + ; ≈-cong = λ _ → let open ≈-Reasoning (A) in refl-hom + }} where + +--- Get a nat on A from a nat on CommaCategory +-- NIA : { I : Category c₁ c₂ ℓ } → ( Γ : Functor I CommaCategory ) (c : Obj CommaCategory ) ( ta : NTrans I CommaCategory ( K CommaCategory I c ) Γ ) → NTrans I A ( K A I (obj c) ) (FIA Γ) NIA {I} Γ c ta = record { @@ -52,6 +73,8 @@ open LimitPreserve +-- Limit on A from Γ : I → CommaCategory +-- LimitC : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I ) → ( Γ : Functor I CommaCategory ) → ( glimit : LimitPreserve A I C G ) @@ -64,7 +87,7 @@ tu : { I : Category c₁ c₂ ℓ } → ( comp : Complete A I) → ( Γ : Functor I CommaCategory ) → NTrans I C (K C I (FObj F (limit-c comp (FIA Γ)))) (G ○ (FIA Γ)) tu {I} comp Γ = record { - TMap = λ i → C [ hom ( FObj Γ i ) o FMap F (frev comp Γ i) ] + TMap = λ i → C [ hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ] ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} } } where commute : {a b : Obj I} {f : Hom I a b} → @@ -143,22 +166,58 @@ 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) Γ ) → + NTrans I C (K C I (FObj F (obj a))) (G ○ FIA Γ) +gnat {I} comp Γ glimit a t = record { + TMap = ? + ; isNTrans = record { commute = ? } + } + comma-a0 : { 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) Γ ) → Hom CommaCategory a (commaLimit comp Γ glimit) comma-a0 {I} comp Γ glimit a t = record { arrow = limit (isLimit ( climit comp (FIA Γ) ) ) (obj a ) (NIA {I} Γ a t ) ; comm = comm1 } where + tcomm : { x y : Obj I } { f : Hom I x y} → A [ A [ FMap (FIA Γ) f o TMap (NIA Γ a t) x ] ≈ A [ TMap (NIA Γ a t) y o id1 A (obj a) ] ] + tcomm {x} {y} {f} = ( IsNTrans.commute ( isNTrans t )) {x} {y} {f} comm1 : C [ C [ FMap G (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) o hom a ] ≈ 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 ≈⟨ {!!} ⟩ - FMap G ((limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o ( {!!} o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) - ≈⟨ assoc ⟩ - (FMap G ((limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t))) o {!!} ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) - ≈↑⟨ car ( 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)) + limit (isLimit (LimitC comp Γ glimit )) (FObj F (obj a)) {!!} + ≈⟨ 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 + 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)) ) + ≈⟨ assoc ⟩ + ( 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)) + ≈⟨ car ( t0f=t ( isLimit (LimitC comp Γ glimit )) ) ⟩ + TMap (tu comp Γ ) i o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) + ≈⟨⟩ + ( hom ( FObj Γ i ) o FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) + o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) + ≈↑⟨ assoc ⟩ + hom ( FObj Γ i ) o + ((FMap F ( TMap (t0 ( climit comp (FIA Γ))) i) ) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ) + ≈↑⟨ cdr ( distr F ) ⟩ + hom ( FObj Γ i ) o + 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 {!!} i ) + ≈⟨ {!!} ⟩ + TMap {!!} i + ∎ + ) ⟩ + 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)) ≈⟨⟩ hom (commaLimit comp Γ glimit) o FMap F (limit (isLimit (climit comp (FIA Γ))) (obj a) (NIA Γ a t)) ∎