Mercurial > hg > Members > kono > Proof > category
view yoneda.agda @ 194:3271d2d04b17
F2Nat→Nat2F done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Aug 2013 19:46:40 +0900 |
| parents | 4e6f080f0107 |
| children | 428d46dfd5aa |
line wrap: on
line source
---- -- -- A → Sets^A^op : Yoneda Functor -- Contravariant Functor h_a -- Nat(h_a,F) -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> ---- open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where open import HomReasoning open import cat-utility open import Relation.Binary.Core open import Relation.Binary -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) open Functor -- A is Locally small postulate ≈-≡ : {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 : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ CF' : (a : Obj A) → Functor A Sets CF' a = record { FObj = λ b → Hom A a b ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] ; isFunctor = record { identity = identity ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g ; ≈-cong = cong1 } } where lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] identity {b} = extensionality lemma-CF1 lemma-CF2 : (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-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( 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 ) ∎ ) distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x ) cong1 : {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ] cong1 eq = extensionality ( λ x → ( ≈-≡ ( (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq ))) open import Function CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂}) CF {a} = record { FObj = λ b → Hom (Category.op A) a b ; FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; isFunctor = record { identity = \{b} → extensionality ( λ x → lemma-CF1 {b} x ) ; distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-CF2 a b c f g x ) ; ≈-cong = λ eq → extensionality ( λ x → lemma-CF3 x eq ) } } where lemma-CF1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL lemma-CF2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin Category.op A [ Category.op A [ g o f ] o x ] ≈↑⟨ assoc ⟩ Category.op A [ g o Category.op A [ f o x ] ] ≈⟨⟩ ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) ∎ ) lemma-CF3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ] lemma-CF3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin Category.op A [ f o x ] ≈⟨ resp refl-hom eq ⟩ Category.op A [ g o x ] ∎ ) YObj = Functor (Category.op A) (Sets {c₂}) YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g y-map : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (CF {a}) x → FObj (CF {b} ) x y-map a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) y-nat : {a b : Obj A } → (f : Hom A a b ) → YHom (CF {a}) (CF {b}) y-nat {a} {b} f = record { TMap = y-map a b f ; isNTrans = isNTrans1 {a} {b} f } where lemma-CF4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → Sets [ Sets [ FMap CF g o y-map a b f a₁ ] ≈ Sets [ y-map a b f b₁ o FMap CF g ] ] lemma-CF4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality ( λ x → ≈-≡ ( begin A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ A [ f o A [ x o g ] ] ∎ ) ) isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) (CF {b}) (y-map a b f ) isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-CF4 {a₁} {b₁} {g} {a} {b} f } open NTrans Yid : {a : YObj} → YHom a a Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) isNTrans1 {a} = record { commute = refl } _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c _+_{a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] ≈⟨ car (nat f) ⟩ Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ∎ isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) _==_ f g = TMap f ≡ TMap g infix 4 _==_ isSetsAop : IsCategory YObj YHom _==_ _+_ Yid isSetsAop = record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym} ; identityL = refl ; identityR = refl ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ; associative = refl } where o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → f == g → h == i → h + f == i + g o-resp-≈ refl refl = refl SetsAop : Category (suc (ℓ ⊔ (suc c₂) ⊔ c₁)) (suc ( ℓ ⊔ (suc c₂) ⊔ c₁)) (c₂ ⊔ c₁) SetsAop = record { Obj = YObj ; Hom = YHom ; _o_ = _+_ ; _≈_ = _==_ ; Id = Yid ; isCategory = isSetsAop } postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ YonedaFunctor : Functor A SetsAop YonedaFunctor = record { FObj = λ a → CF {a} ; FMap = λ f → y-nat f ; isFunctor = record { identity = identity ; distr = distr1 ; ≈-cong = ≈-cong } } where ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ] ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) extensionality1 ( λ x → extensionality ( λ h → ≈-≡ ( begin A [ f o h ] ≈⟨ resp refl-hom eq ⟩ A [ g o h ] ∎ ) ) ) identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} ) ] identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) extensionality1 ( λ x → extensionality ( λ g → ≈-≡ ( begin A [ id1 A a o g ] ≈⟨ idL ⟩ g ∎ ) ) ) distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) extensionality1 ( λ x → extensionality ( λ h → ≈-≡ ( begin A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ A [ g o A [ f o h ] ] ∎ ) ) ) ------ -- -- F : A → Sets ∈ Obj SetsAop -- -- F(a) ⇔ Nat(h_a,F) -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x ------ F2Natmap : {a : Obj A} → {F : Obj SetsAop} → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) b) (FObj F b) F2Natmap {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (CF {a}) F F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} {x} ; isNTrans = isNTrans1 } where commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x commute1 g = let open ≈-Reasoning (Sets) in cong ( λ f → f x ) ( sym ( distr F ) ) commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → Sets [ Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ] commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in begin Sets [ FMap F f o F2Natmap {a} {F} {x} a₁ ] ≈⟨⟩ Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] ≈⟨ extensionality ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap CF f ] ≈⟨⟩ Sets [ F2Natmap {a} {F} {x} b o FMap CF f ] ∎ isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F}) isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (CF {a}) F → FObj F a Nat2F {a} {F} ha = ( TMap ha a ) (id1 A a) F2Nat→Nat2F : {a : Obj A } → {F : Obj SetsAop} → (fa : FObj F a) → Nat2F {a} {F} (F2Nat {a} {F} fa) ≡ fa -- FMap F (Category.Category.Id A) fa ≡ fa F2Nat→Nat2F {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( begin ( FMap F (id1 A _ )) ≈⟨ IsFunctor.identity (isFunctor F) ⟩ id1 Sets (FObj F a) ∎ ) open import Relation.Binary.PropositionalEquality postulate extensionality2 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂ postulate extensionality3 : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] -- (λ b g → FMap F g (TMap ha a (Category.Category.Id A))) ≡ TMap ha Nat2F→F2Nat {a} {F} ha = let open ≡-Reasoning in begin ( λ (b : Obj A ) → λ (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A)) ) ≡⟨ extensionality2 ( λ b → extensionality3 (λ g → lemma1 {a} {F} ha b g )) ⟩ TMap ha ∎ where lemma1 : {a : Obj A } → {F : Obj SetsAop} → (ha : Hom SetsAop (CF {a}) F) → (b : Obj A ) → (g : Hom A b a ) → FMap F g (TMap ha a (Category.Category.Id A)) ≡ TMap ha b g lemma1 {a} {F} ha b g = ? -- F : op A → Sets -- ha : NTrans (op A) Sets (CF {a}) F -- FMap (CF {a}) g o TMap ha a ≈ TMap ha b o FMap F g