Mercurial > hg > Members > kono > Proof > category
view freyd2.agda @ 613:afddfebea797
t0f=t0 done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 13 Jun 2017 22:36:54 +0900 |
parents | f924056bf08a |
children | e6be03d94284 |
line wrap: on
line source
open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets renaming ( _o_ to _*_ ) module freyd2 where open import HomReasoning open import cat-utility open import Relation.Binary.Core open import Function ---------- -- -- a : Obj A -- U : A → Sets -- 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 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 import Relation.Binary.PropositionalEquality -- 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 co Yoneda Functor -- ---- open NTrans open Functor open Limit open IsLimit open import Category.Cat HomA : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) HomA {c₁} {c₂} {ℓ} A a = record { FObj = λ b → Hom A a b ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) ; isFunctor = record { identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) } } where lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin A [ A [ g o f ] o x ] ≈↑⟨ assoc ⟩ A [ g o A [ f o x ] ] ≈⟨⟩ ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) ∎ ) lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin A [ f o x ] ≈⟨ resp refl-hom eq ⟩ A [ g o x ] ∎ ) -- Representable U ≈ Hom(A,-) record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where field -- FObj U x : A → Set -- FMap U f = Set → Set (locally small) -- λ b → Hom (a,b) : A → Set -- λ f → Hom (a,-) = λ b → Hom a b repr→ : NTrans A (Sets {c₂}) U (HomA A a ) repr← : NTrans A (Sets {c₂}) (HomA A a) U reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (HomA A a) x )] reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] 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 -- -- HomA A b = λ a → Hom A a b : Functor A Sets -- : Functor Sets A UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) (Γ : Functor I A) (limita : Limit A I Γ) → IsLimit Sets I (HomA A b ○ Γ) (FObj (HomA A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (HomA A b)) UpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { limit = λ a t → ψ a t ; t0f=t = λ {a t i} → t0f=t0 a t i ; limit-uniqueness = λ {b} {t} {f} t0f=t → {!!} } where hat0 : NTrans I Sets (K Sets I (FObj (HomA A b) (a0 lim))) (HomA A b ○ Γ) hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b) haa0 : Obj Sets haa0 = FObj (HomA A b) (a0 lim) ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) → NTrans I A (K A I b ) Γ ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin FMap Γ f o TMap t a₁ x ≈⟨⟩ ( ( FMap (HomA A b ○ Γ ) f ) * TMap t a₁ ) x ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x ≈⟨⟩ ( TMap t b₁ * id1 Sets a ) x ≈⟨⟩ TMap t b₁ x ≈↑⟨ idR ⟩ TMap t b₁ x o id1 A b ≈⟨⟩ TMap t b₁ x o FMap (K A I b) f ∎ ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (HomA A b ○ Γ)) → Hom Sets X (FObj (HomA A b) (a0 lim)) ψ X t x = FMap (HomA A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (HomA A b ○ Γ)) (i : Obj I) → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ≈ TMap t i ] t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (HomA A b)) i o ψ a t ] ) x ≈⟨⟩ FMap (HomA A b) ( TMap (t0 lim) i) (FMap (HomA A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) ≈⟨⟩ TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) ≈⟨ cdr idR ⟩ TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) ≈⟨ t0f=t (isLimit lim) ⟩ TMap (ta a x t) i ≈⟨⟩ TMap t i x ∎ )) UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) (b : Obj A ) → LimitPreserve A I Sets (HomA A b) UpreserveLimit A I b = record { preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim } -- K{*}↓U has preinitial full subcategory then U is representable -- K{*}↓U is complete, so it has initial object UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A A) (U : Functor A (Sets {c₂}) ) (a : Obj Sets ) (x : Obj ( K (Sets) A a ↓ U) ) ( init : HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U ) x ) → Representable A U (obj x) UisRepresentable A comp U a x init = record { repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } ; reprId→ = λ {y} → ? ; reprId← = λ {y} → ? } -- 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 ) KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (comp : Complete A A) (U : Functor A (Sets) ) (a : Obj A ) (R : Representable A U a ) → HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj U a) ↓ U ) ( record { obj = a ; hom = id1 Sets (FObj U a) } ) KUhasInitialObj A comp U a R = record { initial = λ b → {!!} ; uniqueness = λ b f → {!!} }