Mercurial > hg > Members > kono > Proof > category
changeset 623:bed3be9a4168
One
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Jun 2017 19:11:36 +0900 |
| parents | bd890a43ef5b |
| children | 9b9bc1e076f3 |
| files | Comma.agda freyd2.agda |
| diffstat | 2 files changed, 85 insertions(+), 100 deletions(-) [+] |
line wrap: on
line diff
--- a/Comma.agda Fri Jun 23 10:07:34 2017 +0900 +++ b/Comma.agda Fri Jun 23 19:11:36 2017 +0900 @@ -1,6 +1,6 @@ open import Level open import Category -module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁ c₂ ℓ} {C : Category c₁' c₂' ℓ'} +module Comma {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} {A : Category c₁ c₂ ℓ} {B : Category c₁'' c₂'' ℓ''} {C : Category c₁' c₂' ℓ'} ( F : Functor A C ) ( G : Functor B C ) where open import HomReasoning @@ -13,7 +13,7 @@ open Functor -record CommaObj : Set ( c₁ ⊔ c₂' ) where +record CommaObj : Set ( c₁ ⊔ c₁'' ⊔ c₂' ) where field obj : Obj A objb : Obj B @@ -21,7 +21,7 @@ open CommaObj -record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ ℓ' ) where +record CommaHom ( a b : CommaObj ) : Set ( c₂ ⊔ c₂'' ⊔ ℓ' ) where field arrow : Hom A ( obj a ) ( obj b ) arrowg : Hom B ( objb a ) ( objb b ) @@ -29,7 +29,7 @@ open CommaHom -record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set ℓ where +record _⋍_ { a b : CommaObj } ( f g : CommaHom a b ) : Set (ℓ ⊔ ℓ'' ) where field eqa : A [ arrow f ≈ arrow g ] eqb : B [ arrowg f ≈ arrowg g ] @@ -103,7 +103,7 @@ } } -CommaCategory : Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ +CommaCategory : Category (c₂' ⊔ c₁ ⊔ c₁'') (ℓ' ⊔ c₂ ⊔ c₂'') (ℓ ⊔ ℓ'' ) CommaCategory = record { Obj = CommaObj ; Hom = CommaHom ; _o_ = _∙_
--- a/freyd2.agda Fri Jun 23 10:07:34 2017 +0900 +++ b/freyd2.agda Fri Jun 23 19:11:36 2017 +0900 @@ -17,18 +17,6 @@ -- U ⋍ Hom (a,-) -- ----- --- C is locally small i.e. Hom C i j is a set c₁ --- -record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - hom→ : {i j : Obj C } → Hom C i j → I - hom← : {i j : Obj C } → ( f : I ) → Hom C i j - hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f - -open Small - -- maybe this is a part of local smallness postulate ≈-≡ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y @@ -36,7 +24,6 @@ -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ - ---- -- -- Hom ( a, - ) is Object mapping in Yoneda Functor @@ -94,19 +81,6 @@ open Representable open import freyd -_↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } - → ( F G : Functor A B ) - → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ -_↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory - where open import Comma1 F G - -open import freyd -open SmallFullSubcategory -open Complete -open PreInitial -open HasInitialObject -open import Comma1 -open CommaObj open LimitPreserve -- Representable Functor U preserve limit , so K{*}↓U is complete @@ -189,89 +163,100 @@ -- K{*}↓U has preinitial full subcategory if U is representable -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) +data OneObject {c : Level} : Set c where + OneObj : OneObject + +data OneMor {c : Level} : OneObject {c} → OneObject {c} → Set c where + OneIdMor : OneMor OneObj OneObj + +comp : {A B C : OneObject} → OneMor B C → OneMor A B → OneMor A C +comp OneIdMor OneIdMor = OneIdMor + +OneEquiv : {c : Level} {A B : OneObject {c} } → IsEquivalence {c} {c} {OneMor A B} _≡_ +OneEquiv = record { refl = refl ; sym = ≡-sym; trans = ≡-trans} + +OneID : {A : OneObject} → OneMor A A +OneID {OneObj} = OneIdMor + +OneAssoc : {A B C D : OneObject} {f : OneMor C D} {g : OneMor B C } {h : OneMor A B} + → comp f (comp g h) ≡ comp (comp f g) h +OneAssoc {OneObj} {OneObj} {OneObj} {OneObj} {OneIdMor} {OneIdMor} {OneIdMor} = refl + +OneIdentityL : {A B : OneObject} {f : OneMor A B} → (comp OneID f) ≡ f +OneIdentityL {OneObj} {OneObj} {OneIdMor} = refl + +OneIdentityR : {A B : OneObject} {f : OneMor A B} → (comp f OneID) ≡ f +OneIdentityR {OneObj} {OneObj} {OneIdMor} = refl + +o-resp-≡ : {A B C : OneObject} {f g : OneMor A B} {h i : OneMor B C} → f ≡ g → h ≡ i → comp h f ≡ comp i g +o-resp-≡ {OneObj} {OneObj} {OneObj} {f} {g} {h} {i} f≡g h≡i = + ≡-trans (cong (comp h) f≡g) (cong (λ x → comp x g) h≡i) + + +isCategory : { c : Level } → IsCategory {c} {c} {c} OneObject OneMor _≡_ comp OneID +isCategory = record { isEquivalence = OneEquiv + ; identityL = OneIdentityL + ; identityR = OneIdentityR + ; o-resp-≈ = o-resp-≡ + ; associative = OneAssoc + } + +ONE : { c : Level } → Category c c c +ONE = record { Obj = OneObject + ; Hom = OneMor + ; _≈_ = _≡_ + ; Id = OneID + ; isCategory = isCategory + } + +_↓_ : { c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } { C : Category c₁'' c₂'' ℓ'' } + → ( F : Functor A C ) + → ( G : Functor B C ) + → Category (c₂'' ⊔ c₁ ⊔ c₁') (ℓ'' ⊔ c₂ ⊔ c₂') ( ℓ ⊔ ℓ' ) +_↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} {c₁''} {c₂''} {ℓ''} {A} {B} {C} F G = CommaCategory + where open import Comma F G + +open import freyd +open SmallFullSubcategory +open Complete +open PreInitial +open HasInitialObject +open import Comma +open CommaObj open CommaHom KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) - → HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj (Yoneda A a) a) ↓ (Yoneda A a) ) ( record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } ) + → HasInitialObject {c₁} {c₂} {ℓ} ( K Sets ONE OneObject ↓ (Yoneda A a) ) ( record { obj = OneObj ; hom = {!!} } ) KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { initial = λ b → initial0 b - ; uniqueness = λ b f → unique b f + ; uniqueness = {!!} } where commaCat : Category (c₂ ⊔ c₁) c₂ ℓ - commaCat = K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a - initObj : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) - initObj = record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } - hom1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → - Hom Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) (FObj (Yoneda A a) (obj b)) - hom1 b = λ (x : Hom A a a ) → hom b x - hom2 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b ) - hom2 b x = hom b x - hom3 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a (obj b ) - hom3 b = hom b (id1 A a) - hom4 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → Hom A a a → Hom A a (obj b ) - hom4 b x = A [ hom b (id1 A a) o x ] - comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (x : FObj (Yoneda A a ) a ) - → A [ ( Sets [ FMap (Yoneda A a) (id1 A (obj b) ) o hom b ] ) x ≈ hom b x ] - comm1 b x = let open ≈-Reasoning A in ≡-≈ ( cong ( λ k -> k x ) ( comm ( id1 (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a)) b ) ) ) - -- hom b is Hom A a a → Hom A a (obj b) - -- hom b x is ( x : Hom A a a ) → Hom A a (obj b) - -- hom b (id1 A a) is ( id1 A a : Hom A a a ) → Hom A a (obj b) - -- hom b (id1 A a) o x is ( x : Hom A a a ) → Hom A a (obj b) - -- x - -- a ----> a -> obj b hom b x - -- - -- x id - -- a ----> a -> obj b hom b (id a) o x - -- - initial0comm1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a ) - → FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x + commaCat = K Sets ONE OneObject ↓ Yoneda A a + initObj : Obj (K Sets ONE OneObject ↓ Yoneda A a) + initObj = record { obj = OneObj ; hom = {!!} } + initial0comm1 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → (x : {!!} ) + → FMap (Yoneda A a) (hom b {!!}) x ≡ hom b {!!} initial0comm1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin - FMap (Yoneda A a) (hom b (id1 A a)) x + FMap (Yoneda A a) (hom b {!!}) x ≈⟨⟩ - hom b (id1 A a ) o x + hom b {!!} o x ≈⟨ {!!} ⟩ - hom b x + hom b {!!} ∎ ) - initial0comm : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → - Sets [ Sets [ FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ] ≈ - Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) ] ] + initial0comm : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → + Sets [ Sets [ FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) ] ≈ {!!} ] initial0comm b = let open ≈-Reasoning Sets in begin - FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) - ≈⟨⟩ - FMap (Yoneda A a) (hom b (id1 A a)) - ≈⟨ extensionality A ( λ x → initial0comm1 b x ) ⟩ - hom b - ≈⟨⟩ - hom b o id1 Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) - ≈⟨⟩ - hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) + FMap (Yoneda A a) (hom b {!!}) o id1 Sets (FObj (Yoneda A a) a) + ≈⟨ {!!} ⟩ + {!!} ∎ - initial0 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → - Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a)) initObj b + initial0 : (b : Obj (K Sets ONE OneObject ↓ (Yoneda A a))) → + Hom (K Sets ONE OneObject ↓ (Yoneda A a)) initObj b initial0 b = record { - arrow = hom b (id1 A a) - ; comm = initial0comm b } - -- what is comm f ? - comm-f : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) - (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b) - → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] - ≈ Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ] - comm-f b f = comm f - unique : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a)) - (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) initObj b) - → (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) [ f ≈ initial0 b ] - unique b f = let open ≈-Reasoning A in begin - arrow f - ≈↑⟨ idR ⟩ - arrow f o id1 A a - ≈⟨⟩ - ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) - ≈⟨ ≡-≈ ( cong (λ k → k (id1 A a)) (comm f ) ) ⟩ - ( Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ) (id1 A a) - ≈⟨⟩ - hom b (id1 A a) - ∎ + arrow = {!!} + ; comm = {!!} } -- K{*}↓U has preinitial full subcategory then U is representable @@ -283,7 +268,7 @@ -- (U : Functor A (Sets {c₂}) ) -- (a : Obj (Sets {c₂})) (ax : a) -- (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) ) --- (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) +-- (PI : PreInitial {c₁} {c₂} {ℓ} ( K Sets ONE OneObject ↓ U) (SFSF SFS )) -- → Representable A U (obj (preinitialObj PI )) -- UisRepresentable A U a ax SFS PI = record { -- repr→ = record { TMap = tmap1 ; isNTrans = record { commute = {!!} } }