Mercurial > hg > Members > kono > Proof > category

annotate yoneda.agda @ 183:ea6fc610b480

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Contravariant functor done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 28 Aug 2013 17:29:01 +0900
parents 346e8eb35ec3
children d2d749318bee
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Category -- https://github.com/konn/category-agda
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Category.Sets
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import HomReasoning
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import cat-utility
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
8 open import Relation.Binary.Core
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
9 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
10
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} )
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
13 open Functor
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
181
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
15 -- A is Locally small
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
16 postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
17
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
18 import Relation.Binary.PropositionalEquality
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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 )
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
20 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
21
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 ; ≈-cong = cong1
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 }
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 } where
181
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
33 lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
36 identity {b} = extensionality lemma-CF1
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
38 lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
39 A [ A [ g o f ] o x ]
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
40 ≈↑⟨ assoc ⟩
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
41 A [ g o A [ f o x ] ]
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
42 ≈⟨⟩
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
43 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x )
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
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
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
49 cong1 eq = extensionality ( λ x → ( ≈-≡ (
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
50 (IsCategory.o-resp-≈ ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A ))) eq )))
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
182
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
52 open import Function
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
182
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
54 CF : (a : Obj A) → Functor (Category.op A) Sets
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
55 CF a = record {
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