Mercurial > hg > Members > kono > Proof > category

annotate yoneda.agda @ 190:b82d7b054f28

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
one to one nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2013 16:07:45 +0900
parents c6ce3115cb1b
children 45191dc3f78a
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
1 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
2 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
3 -- A → Sets^A^op : Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
4 -- Contravariant Functor h_a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
5 -- Nat(h_a,F)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
7 ----
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
8
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Category -- https://github.com/konn/category-agda
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Level
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Category.Sets
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import HomReasoning
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import cat-utility
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
16 open import Relation.Binary.Core
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
17 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
18
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} )
179
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 178
diff changeset
21 open Functor
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
181
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
23 -- A is Locally small
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
24 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
25
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
26 import Relation.Binary.PropositionalEquality
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
27 -- 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
28 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
29
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
30
182
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
31 CF' : (a : Obj A) → Functor A Sets
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
32 CF' a = record {
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 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
34 ; 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
35 ; isFunctor = record {
180
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
36 identity = identity
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
37 ; 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
38 ; ≈-cong = cong1
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 }
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 } where
181
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
41 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
42 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
43 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
44 identity {b} = extensionality lemma-CF1
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
45 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
46 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
47 A [ A [ g o f ] o x ]
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
48 ≈↑⟨ assoc ⟩
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
49 A [ g o A [ f o x ] ]
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
50 ≈⟨⟩
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
51 ( λ 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
52 ∎ )
180
2d983d843e29 no yellow on co-Contravariant Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 179
diff changeset
53 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
54 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
55 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
56 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
57 cong1 eq = extensionality ( λ x → ( ≈-≡ (
b58453d90db6 contravariant functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 180
diff changeset
58 (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
59
182
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
60 open import Function
178
6626a7cd9129 Yoneda Functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
62 CF : {a : Obj A} → Functor (Category.op A) (Sets {c₂})
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
63 CF {a} = record {
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
64 FObj = λ b → Hom (Category.op A) a b ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
65 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
66 isFunctor = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
67 identity = \{b} → extensionality ( λ x → lemma-CF1 {b} x ) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
68 distr = λ {a} {b} {c} {f} {g} → extensionality ( λ x → lemma-CF2 a b c f g x ) ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
69 ≈-cong = λ eq → extensionality ( λ x → lemma-CF3 x eq )
182
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
70 }
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
71 } where
346e8eb35ec3 contravariant continue ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 181
diff changeset
72 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
73 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
74 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
75 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
76 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
77 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
78 ≈↑⟨ assoc ⟩
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
79 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
80 ≈⟨⟩
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
81 ( λ 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
82 ∎ )
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
83 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
84 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
85 Category.op A [ f o x ]
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
86 ≈⟨ resp refl-hom eq ⟩
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
87 Category.op A [ g o x ]
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
88 ∎ )
ea6fc610b480 Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 182
diff changeset
89
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
90 YObj = Functor (Category.op A) (Sets {c₂})
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
91 YHom = λ (f : YObj ) → λ (g : YObj ) → NTrans (Category.op A) Sets f g
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
92
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
93 y-map : ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → FObj (CF {a}) x → FObj (CF {b} ) x
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
94 y-map a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b )
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
95
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
96 y-nat : {a b : Obj A } → (f : Hom A a b ) → YHom (CF {a}) (CF {b})
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
97 y-nat {a} {b} f = record { TMap = y-map a b f ; isNTrans = isNTrans1 {a} {b} f } where
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
98 lemma-CF4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
99 Sets [ Sets [ FMap CF g o y-map a b f a₁ ] ≈
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
100 Sets [ y-map a b f b₁ o FMap CF g ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
101 lemma-CF4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality ( λ x → ≈-≡ ( begin
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
102 A [ A [ f o x ] o g ]
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
103 ≈↑⟨ assoc ⟩
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
104 A [ f o A [ x o g ] ]
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
105 ∎ ) )
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
106 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 )
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
107 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-CF4 {a₁} {b₁} {g} {a} {b} f }
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
108
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
109 open NTrans
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
110 Yid : {a : YObj} → YHom a a
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
111 Yid {a} = record { TMap = \a -> \x -> x ; isNTrans = isNTrans1 {a} } where
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
112 isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (\a -> \x -> x )
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
113 isNTrans1 {a} = record { commute = refl }
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
114
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
115 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c
185
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
116 _+_{a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
117 commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b )
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
118 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) →
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
119 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
120 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
121 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
122 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
123 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
124 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
125 ≈⟨ car (nat f) ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
126 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
127 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
128 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
129 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
130 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
131 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
132 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ]
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
133 ∎
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
134 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ])
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
135 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
136
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
137 _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁)
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
138 _==_ f g = TMap f ≡ TMap g
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
139
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
140 infix 4 _==_
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
141
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
142 isSetsAop : IsCategory YObj YHom _==_ _+_ Yid
189
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
143 isSetsAop =
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
144 record { isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
145 ; identityL = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
146 ; identityR = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
147 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
148 ; associative = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
149 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
150 o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
151 f == g → h == i → h + f == i + g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
152 o-resp-≈ refl refl = refl
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
153
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
154 SetsAop : Category (suc (ℓ ⊔ (suc c₂) ⊔ c₁)) (suc ( ℓ ⊔ (suc c₂) ⊔ c₁)) (c₂ ⊔ c₁)
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
155 SetsAop =
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
156 record { Obj = YObj
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
157 ; Hom = YHom
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
158 ; _o_ = _+_
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
159 ; _≈_ = _==_
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
160 ; Id = Yid
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
161 ; isCategory = isSetsAop
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
162 }
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
163
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
164 postulate extensionality1 : Relation.Binary.PropositionalEquality.Extensionality c₁ c₂
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
165
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
166 YonedaFunctor : Functor A SetsAop
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
167 YonedaFunctor = record {
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
168 FObj = λ a → CF {a}
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
169 ; FMap = λ f → y-nat f
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
170 ; isFunctor = record {
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
171 identity = identity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
172 ; distr = distr1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
173 ; ≈-cong = ≈-cong
186
b2e01aa0924d y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 185
diff changeset
174 }
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
175 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
176 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ]
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
177 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] )
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
178 extensionality1 ( λ x → extensionality (
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
179 λ h → ≈-≡ ( begin
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
180 A [ f o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
181 ≈⟨ resp refl-hom eq ⟩
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
182 A [ g o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
183 ∎
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
184 ) ) )
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
185 identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} ) ]
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
186 identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
187 extensionality1 ( λ x → extensionality (
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
188 λ g → ≈-≡ ( begin
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
189 A [ id1 A a o g ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
190 ≈⟨ idL ⟩
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
191 g
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
192 ∎
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
193 ) ) )
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
194 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 ] ]
188
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
195 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₁ ] ] )
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
196 extensionality1 ( λ x → extensionality (
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
197 λ h → ≈-≡ ( begin
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
198 A [ A [ g o f ] o h ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
199 ≈↑⟨ assoc ⟩
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
200 A [ g o A [ f o h ] ]
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
201 ∎
f4c9d7cbcbb9 Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
202 ) ) )
184
d2d749318bee oeration
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
203
185
173d078ee443 Yoneda join
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 184
diff changeset
204
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
205 ------
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
206 --
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
207 -- F : A → Sets ∈ Obj SetsAop
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
208 --
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
209 -- F(a) ⇔ Nat(h_a,F)
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
210 --
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
211 ------
187
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 186
diff changeset
212
190
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
213 F2Natmap : {a : Obj A} → {F : Obj SetsAop} → (x : Obj (Category.op A)) → Hom Sets (FObj (CF {a}) x) (FObj F x)
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
214 F2Natmap = {!!}
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
215
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
216 F2Nat : {a : Obj A} → {F : Obj SetsAop} → FObj F a → Hom SetsAop (CF {a}) F
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
217 F2Nat {a} {F} x = record { TMap = F2Natmap {a} {F} ; isNTrans = isNTrans1 {a} } where
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
218 isNTrans1 : {a : Obj A } → IsNTrans (Category.op A) (Sets {c₂}) (CF {a}) F (F2Natmap {a} {F})
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
219 isNTrans1 {a} = record { commute = {!!} }
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
220
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
221
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
222 Nat2F : {a : Obj A} → {F : Obj SetsAop} → Hom SetsAop (CF {a}) F → FObj F a
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
223 Nat2F = {!!}
b82d7b054f28 one to one nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
224