Mercurial > hg > Members > kono > Proof > category
changeset 508:3ce21b2a671a
IProduct is written in Sets
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 18 Mar 2017 16:15:40 +0900 |
| parents | c1c12e5a82ad |
| children | 3e82fb1ce170 |
| files | SetsCompleteness.agda cat-utility.agda limit-to.agda pullback.agda |
| diffstat | 4 files changed, 60 insertions(+), 40 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Fri Mar 17 19:55:51 2017 +0900 +++ b/SetsCompleteness.agda Sat Mar 18 16:15:40 2017 +0900 @@ -39,6 +39,22 @@ prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl +record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where + field + pi1 : ( i : I ) → pi0 i + +open iproduct + + +SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) + → IProduct ( Sets { c₂} ) I +SetsIProduct I fi = record { + ai = fi + ; iprod = iproduct I fi + ; pi = λ i prod → pi1 prod i + ; isIProduct = {!!} + } + SetsEqualizer : { c₂ : Level} → {a b : Obj (Sets {c₂}) } (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g SetsEqualizer f g = record { equalizer-c = {!!} @@ -54,9 +70,9 @@ open Functor open NTrans -record ΓObj { c₂ } (x : Set c₂ ) : Set c₂ where +record ΓObj { c₂ } ( I : Set c₂ ) : Set c₂ where field - obj : x + obj : I open ΓObj @@ -66,48 +82,39 @@ open ΓMap +fmap : { c₂ : Level} {a b : Set c₂ } → (f : a → b ) → ΓMap f +fmap {a} {b} f = record { map = λ aobj → record { obj = f ( obj aobj ) } } -record Slimit { c₂ } ( sobj : Set c₂ → Set c₂ ) (smap : {a b : Set c₂ } ( f : a → b ) → Set c₂ ) - : Set c₂ where --- field --- aap : ΓObj slim --- ap : ΓObj slim → ΓObj slim --- hoge : sobj slim --- hoge1 : smap {slim} {slim} ( λ x → x ) - -record ΓTMap { c₂ } (a : Set c₂ ) : Set c₂ where - field - tmap : a → Slimit ΓObj ΓMap → ΓObj a - -open ΓTMap +Γ : { c₂ : Level } → Functor (Sets { c₂}) (Sets { c₂}) +Γ { c₂} = record { FObj = ΓObj ; FMap = ( λ f → map (fmap f )) ; isFunctor = record { + identity = λ {b} → refl ; + distr = λ {a} {b} {c} {f} {g} → refl ; + ≈-cong = cong1 + } } where + cong1 : {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ] + cong1 refl = refl --- sobj : S --- smap : fobj S --- hoge : ΓObj S - --- bb : ΓObj I --- cc : I → I +record Slimit { c₂ } (I : Set c₂) ( sobj : Set c₂ → Set c₂ ) (smap : { a b : Set c₂ } ( f : a → b ) → Set c₂ ) + : Set c₂ where + field + s-t0 : (i : I ) → sobj ? open Slimit -tmp : { c₂ : Level} {a b : Set c₂ } → (f : a → b ) → ΓMap f -tmp {a} {b} f = record { map = λ aobj → record { obj = f ( obj aobj ) } } - -ttmp : {c₂ : Level} (A : Set c₂ ) → ΓTMap A -ttmp A = record { tmap = λ a slim → record { obj = a } } - -SetsLimit : { c₂ : Level} (e : Set c₂) ( Γ : IsFunctor (Sets { c₂}) (Sets { c₂}) ΓObj ( λ f → map (tmp f ) )) - → Limit Sets Sets ( record { FObj = ΓObj ; FMap = ( λ f → map (tmp f )) ; isFunctor = Γ } ) -SetsLimit { c₂} e Γ = record { - a0 = Slimit ΓObj ΓMap - ; t0 = record { TMap = λ i → {!!} ; isNTrans = record { commute = {!!} } } +SetsLimit : { c₂ : Level} → Limit Sets Sets Γ +SetsLimit { c₂} = record { + a0 = Slimit (Obj Sets) ΓObj ΓMap + ; t0 = record { + TMap = λ i → λ lim → s-t0 lim ? + ; isNTrans = record { commute = {!!} } + } ; isLimit = record { limit = {!!} ; t0f=t = {!!} ; limit-uniqueness = {!!} } - } where - tmap0 : (a : Obj Sets) → Hom Sets (FObj (K Sets Sets ( Slimit ΓObj ΓMap)) a) (ΓObj a) - tmap0 a oa = tmap ( ttmp a ) ? oa - + } where +-- comm1 : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → s-t0 lim ? ) ] ≈ +-- Sets [ (λ lim → s-t0 lim ?) o FMap (K Sets Sets (Slimit (Obj Sets) ΓObj (λ {a} {b} → ΓMap))) f ] ] + -- comm1 {a} {b} {f} = {!!}
--- a/cat-utility.agda Fri Mar 17 19:55:51 2017 +0900 +++ b/cat-utility.agda Sat Mar 18 16:15:40 2017 +0900 @@ -221,10 +221,10 @@ -- product on arbitrary index -- - record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) + record IsIProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) ( p : Obj A ) -- product ( ai : I → Obj A ) -- families - ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections + ( pi : (i : I ) → Hom A p ( ai i ) ) -- projections : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where field iproduct : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → Hom A q p @@ -248,6 +248,13 @@ iproduct qi ∎ + record IProduct { c c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Set c) : Set (c ⊔ ℓ ⊔ (c₁ ⊔ c₂)) where + field + ai : I → Obj A + iprod : Obj A + pi : (i : I ) → Hom A iprod ( ai i ) + isIProduct : IsIProduct A I iprod ai pi + -- Pullback -- f
--- a/limit-to.agda Fri Mar 17 19:55:51 2017 +0900 +++ b/limit-to.agda Sat Mar 18 16:15:40 2017 +0900 @@ -270,12 +270,17 @@ lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ ) (comp : Complete A ( DiscreteCat S ) ) → ( Γ : Functor (DiscreteCat S ) A ) - → IProduct A (Obj ( DiscreteCat S ) )(plimit A S comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i ) + → IProduct A (Obj ( DiscreteCat S ) ) -- (plimit A S comp Γ) (λ i → FObj Γ i ) ( λ i → TMap (limit-u comp Γ) i ) lim-to-product A S comp Γ = record { + ai = λ i → FObj Γ i + ; iprod = plimit A S comp Γ + ; pi = λ i → TMap (limit-u comp Γ) i + ; isIProduct = record { iproduct = λ {q} qi → iproduct {q} qi ; pif=q = λ {q } qi { i } → pif=q {q} qi {i} ; ip-uniqueness = λ {q } { h } → ip-uniqueness {q} {h} ; ip-cong = λ {q } { qi } { qi' } qi=qi' → ip-cong {q} {qi} {qi'} qi=qi' + } } where D = DiscreteCat S I = Obj ( DiscreteCat S )
--- a/pullback.agda Fri Mar 17 19:55:51 2017 +0900 +++ b/pullback.agda Sat Mar 18 16:15:40 2017 +0900 @@ -301,6 +301,7 @@ open IProduct +open IsIProduct open Equalizer -- @@ -350,7 +351,7 @@ limit-from : ( prod : (p : Obj A) ( ai : Obj I → Obj A ) ( pi : (i : Obj I) → Hom A p ( ai i ) ) - → IProduct {c₁'} A (Obj I) p ai pi ) + → IsIProduct {c₁'} A (Obj I) p ai pi ) ( eqa : {a b c : Obj A} → (e : Hom A c a ) → (f g : Hom A a b) → IsEqualizer A e f g ) ( lim p : Obj A ) -- limit to be made ( e : Hom A lim p ) -- existing of equalizer