Mercurial > hg > Members > kono > Proof > category
annotate yoneda.agda @ 184:d2d749318bee
oeration
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Aug 2013 18:28:23 +0900 |
| parents | ea6fc610b480 |
| children | 173d078ee443 |
| rev | line source |
|---|---|
| 178 | 1 open import Category -- https://github.com/konn/category-agda |
| 2 open import Level | |
| 3 open import Category.Sets | |
| 4 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where | |
| 5 | |
| 6 open import HomReasoning | |
| 7 open import cat-utility | |
| 179 | 8 open import Relation.Binary.Core |
| 9 open import Relation.Binary | |
| 10 | |
| 178 | 11 |
| 12 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) | |
| 179 | 13 open Functor |
| 178 | 14 |
| 181 | 15 -- A is Locally small |
| 16 postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y | |
| 17 | |
| 18 import Relation.Binary.PropositionalEquality | |
| 19 -- 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 ) | |
| 20 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ | |
| 21 | |
| 22 | |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
23 CF' : (a : Obj A) → Functor A Sets |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
24 CF' a = record { |
| 178 | 25 FObj = λ b → Hom A a b |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
26 ; FMap = λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) → A [ f o g ] |
| 178 | 27 ; isFunctor = record { |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
28 identity = identity |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
29 ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g |
| 178 | 30 ; ≈-cong = cong1 |
| 31 } | |
| 32 } where | |
| 181 | 33 lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
| 34 lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
35 identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ] |
| 181 | 36 identity {b} = extensionality lemma-CF1 |
| 37 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 | |
| 38 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin | |
| 39 A [ A [ g o f ] o x ] | |
| 40 ≈↑⟨ assoc ⟩ | |
| 41 A [ g o A [ f o x ] ] | |
| 42 ≈⟨⟩ | |
| 43 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) | |
| 44 ∎ ) | |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
45 distr1 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → |
|
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
46 Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ] |
| 181 | 47 distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x ) |
|
180
2d983d843e29
no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
179
diff
changeset
|
48 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₁ ]) ] |
| 181 | 49 cong1 eq = extensionality ( λ x → ( ≈-≡ ( |
| 50 (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq ))) | |
| 178 | 51 |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
52 open import Function |
| 178 | 53 |
| 184 | 54 CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂}) |
| 55 CF {a} = record { | |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
56 FObj = λ b → Hom (Category.op A) a b |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
57 ; FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
58 ; isFunctor = record { |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
59 identity = \{b} → extensionality ( λ x → lemma-CF1 {b} x ) |
|
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
60 ; distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-CF2 a b c f g x ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
61 ; ≈-cong = λ eq → extensionality ( λ x → lemma-CF3 x eq ) |
|
182
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
62 } |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
63 } where |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
64 lemma-CF1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x |
|
346e8eb35ec3
contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
181
diff
changeset
|
65 lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL |
|
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
66 lemma-CF2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
67 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
68 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
69 Category.op A [ Category.op A [ g o f ] o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
70 ≈↑⟨ assoc ⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
71 Category.op A [ g o Category.op A [ f o x ] ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
72 ≈⟨⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
73 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
74 ∎ ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
75 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 ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
76 lemma-CF3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ ( begin |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
77 Category.op A [ f o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
78 ≈⟨ resp refl-hom eq ⟩ |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
79 Category.op A [ g o x ] |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
80 ∎ ) |
|
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
81 |
| 184 | 82 YObj = Functor (Category.op A) (Sets {c₂}) |
| 83 YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g | |
| 84 | |
| 85 open NTrans | |
| 86 Yid : {a : YObj} → YHom a a | |
| 87 Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where | |
| 88 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x ) | |
| 89 isNTrans1 {a} = record { commute = refl } | |
| 90 | |
| 91 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c | |
| 92 _+_ = {!!} | |
| 93 | |
| 94 isSetsAop : IsCategory YObj YHom _≡_ _+_ Yid | |
| 95 isSetsAop = {!!} | |
| 96 |