Mercurial > hg > Members > kono > Proof > category
changeset 350:c483374f542b
try equalizer from limit
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 24 Dec 2014 12:00:16 +0900 |
| parents | 5858351ac1b9 |
| children | 1306fbc8290b |
| files | cat-utility.agda freyd.agda limit-to.agda system-f.agda |
| diffstat | 4 files changed, 88 insertions(+), 28 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sun May 04 11:01:36 2014 +0900 +++ b/cat-utility.agda Wed Dec 24 12:00:16 2014 +0900 @@ -161,6 +161,15 @@ -- μR=μ : {x : Obj A } → A [ TMap μR x ≈ TMap μ x ] + -- + -- e f + -- c -------→ a ---------→ b + -- ^ . ---------→ + -- | . g + -- |k . + -- | . h + -- d + record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
--- a/freyd.agda Sun May 04 11:01:36 2014 +0900 +++ b/freyd.agda Wed Dec 24 12:00:16 2014 +0900 @@ -36,6 +36,7 @@ uniqueness : ( a : Obj A ) → ( f : Hom A i a ) → A [ f ≈ initial a ] + -- A complete catagory has initial object if it has PreInitial-SmallFullSubcategory open NTrans @@ -57,15 +58,12 @@ initialArrow a = A [ preinitialArrow PI {a} o limit (lim F {FObj F (preinitialObj PI)} {u (FObj F (preinitialObj PI))} ) a0 (u a0 ) ] lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ] lemma1 a f = let open ≈-Reasoning (A) in + sym ( begin - f - ≈↑⟨ idR ⟩ - f o id1 A a0 + initialArrow a + ≈⟨⟩ + preinitialArrow PI {a} o limit (lim F) a0 (u a0) ≈⟨ {!!} ⟩ - ( preinitialArrow PI {a} o limit (lim F) a0 (u a0)) o id1 A a0 - ≈⟨ idR ⟩ - preinitialArrow PI {a} o limit (lim F) a0 (u a0) - ≈⟨⟩ - initialArrow a - ∎ + f + ∎ )
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/limit-to.agda Wed Dec 24 12:00:16 2014 +0900 @@ -0,0 +1,56 @@ +open import Category -- https://github.com/konn/category-agda +open import Level + +module limit-to {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + where + +open import cat-utility +open import HomReasoning +open import Relation.Binary.Core +open import Category.Sets +open Functor + + +-- If we have limit then we have equalizer +--- two objects category +--- +--- f +--- ------> +--- 0 1 +--- ------> +--- g + +record TwoCat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (a b : Obj A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + f→ : Obj A → Hom A a b + f← : Hom A a b → Obj A + unique-f : (f← (f→ a) ) ≡ a + g→ : Obj A → Hom A a b + g← : Hom A a b → Obj A + unique-g : (g← (g→ b) ) ≡ b + + +open Limit + +lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) + ( i0 i1 : Obj I) + (two : TwoCat I i0 i1) ( Γ : Functor I A ) + (lim : ( Γ : Functor I A ) → { a0 : Obj A } { u : NTrans I A ( K A I a0 ) Γ } → Limit A I Γ a0 u ) -- completeness + → {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → (fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] ) → Equalizer A e f g +lim-to-equ A I i0 i1 two Γ lim {a} {b} {c} f g e fe=ge = record { + fe=ge = fe=ge + ; k = λ {d} h fh=gh → k {d} h fh=gh + ; ek=h = λ {d} {h} {fh=gh} → {!!} + ; uniqueness = λ {d} {h} {fh=gh} {k'} → {!!} + } where + nat : (d : Obj A) → NTrans I A (K A I d) Γ + nat d = record { + TMap = λ x → {!!} ; + isNTrans = record { + commute = {!!} + } + } + 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 (lim Γ {c} {nat c}) d (nat d) +
--- a/system-f.agda Sun May 04 11:01:36 2014 +0900 +++ b/system-f.agda Wed Dec 24 12:00:16 2014 +0900 @@ -1,10 +1,12 @@ +{-# OPTIONS --universe-polymorphism #-} + open import Level open import Relation.Binary.PropositionalEquality module system-f where -Bool : {l : Level} (X : Set l) → Set l -Bool = λ{l : Level} → λ(X : Set l) → X → X → X +Bool : {l : Level} → Set l → Set l +Bool {l} = λ(X : Set l) → X → X → X T : {l : Level} (X : Set l) → Bool X T X = λ(x y : X) → x @@ -23,7 +25,7 @@ _×_ : {l : Level} → Set l → Set l → Set (suc l) _×_ {l} U V = {X : Set l} → (U → V → X) → X - + <_,_> : {l : Level} {U V : Set l} → U → V → (U × V) <_,_> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v @@ -57,33 +59,28 @@ --lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε t (U → V) ) u ≡ ε t V --lemma103 u t = e1 t u -Emp : {l : Level } → Set l → Set l -Emp {l} = λ X → X - --- Emp is not allowed because Emp is not a Set of any level +Emp : {l : Level } → Set (suc l) +Emp {l} = {X : Set l} → X --- ε : {l : Level} (U : Set l) → Emp → U --- ε {l} U t = t U +-- ε : {l : Level} {U : Set l} → Emp {l} → U +-- ε {l} {U} t = t U --- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp ) → (ε (U → V) t) u ≡ ε V t +-- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t -- lemma103 u t = refl --- lemma09 : {l : Level} {U : Set l} → (t : Emp ) → ε U (ε Emp t) ≡ ε U t +-- lemma09 : {l : Level} {U : Set l} → (t : Emp ) → ε {l} {U} (ε {_} {Emp} t) ≡ ε {_} {U} t -- lemma09 t = refl --- lemma10 : {l : Level} {U V X : Set l} → (t : Emp ) → U × V --- lemma10 {l} {U} {V} t = ε (U × V) t - --- lemma10' : {l : Level} {U V X : Set l} → (t : Emp ) → Emp --- lemma10' {l} {U} {V} {X} t = ε (U × V) t +-- lemma10 : {l : Level} {U V X : Set l} → (t : Emp ) → U × V +-- lemma10 {l} {U} {V} t = ε {suc l} {U × V} t -- lemma100 : {l : Level} {U V X : Set l} → (t : Emp ) → Emp --- lemma100 {l} {U} {V} t = ε U t +-- lemma100 {l} {U} {V} t = ε {_} {U} t --- lemma101 : {l k : Level} {U V : Set l} → (t : Emp ) → π1 (ε (U × V) t) ≡ ε U t +-- lemma101 : {l : Level} {U V : Set l} → (t : Emp ) → π1 (ε {suc l} {U × V} t) ≡ ε {l} {U} t -- lemma101 t = refl --- lemma102 : {l k : Level} {U V : Set l} → (t : Emp ) → π2 (ε (U × V) t) ≡ ε V t +-- lemma102 : {l : Level} {U V : Set l} → (t : Emp ) → π2 (ε {_} {U × V} t) ≡ ε {_} {V} t -- lemma102 t = refl