Mercurial > hg > Members > kono > Proof > category
annotate yoneda.agda @ 804:2716d2945730
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Apr 2019 12:22:03 +0900 |
| parents | bded2347efa4 |
| children | 232cea484067 |
| rev | line source |
|---|---|
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
1 --- |
| 189 | 2 -- |
| 3 -- A → Sets^A^op : Yoneda Functor | |
| 4 -- Contravariant Functor h_a | |
| 5 -- Nat(h_a,F) | |
| 6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
| 7 ---- | |
| 8 | |
| 178 | 9 open import Category -- https://github.com/konn/category-agda |
| 10 open import Level | |
| 11 open import Category.Sets | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
12 module yoneda where |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
13 -- { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where |
| 178 | 14 |
| 15 open import HomReasoning | |
| 16 open import cat-utility | |
| 179 | 17 open import Relation.Binary.Core |
| 18 open import Relation.Binary | |
| 781 | 19 open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) |
| 20 | |
| 179 | 21 |
| 178 | 22 |
| 23 -- Contravariant Functor : op A → Sets ( Obj of Sets^{A^op} ) | |
| 197 | 24 -- Obj and Hom of Sets^A^op |
| 181 | 25 |
| 197 | 26 open Functor |
|
183
ea6fc610b480
Contravariant functor done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
182
diff
changeset
|
27 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
28 YObj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
29 YObj {_} {c₂} A = Functor (Category.op A) (Sets {c₂}) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
30 YHom : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (f : YObj A ) → (g : YObj A ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
31 YHom {_} {c₂} A f g = NTrans (Category.op A) (Sets {c₂}) f g |
| 184 | 32 |
| 33 open NTrans | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
34 Yid : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : YObj A } → YHom A a a |
| 300 | 35 Yid {_} {c₂} A {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where |
| 36 isNTrans1 : {a : YObj A } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) | |
| 184 | 37 isNTrans1 {a} = record { commute = refl } |
| 38 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
39 _+_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b c : YObj A} → YHom A b c → YHom A a b → YHom A a c |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
40 _+_ {_} {c₂} {_} {A} {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
41 commute1 : (a b c : YObj A ) (f : YHom A b c) (g : YHom A a b ) |
| 185 | 42 (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → |
| 43 Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ | |
| 44 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] | |
| 45 commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin | |
| 46 Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] | |
| 47 ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ | |
| 48 Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] | |
| 49 ≈⟨ car (nat f) ⟩ | |
| 50 Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] | |
| 51 ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ | |
| 52 Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] | |
| 53 ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ | |
| 54 Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] | |
| 55 ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ | |
| 56 Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] | |
| 57 ∎ | |
| 58 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) | |
| 59 isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } | |
| 184 | 60 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
61 _==_ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : YObj A} → YHom A a b → YHom A a b → Set (c₂ ⊔ c₁) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
62 _==_ {_} { c₂} {_} {A} f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
63 |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
64 infix 4 _==_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
65 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
66 isSetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → IsCategory (YObj A) (YHom A) _==_ _+_ ( Yid A ) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
67 isSetsAop {_} {c₂} {_} A = |
| 300 | 68 record { isEquivalence = record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} |
| 189 | 69 ; identityL = refl |
| 70 ; identityR = refl | |
| 71 ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} | |
| 72 ; associative = refl | |
| 358 | 73 } where |
| 74 open ≈-Reasoning (Sets {c₂}) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
75 sym1 : {a b : YObj A } {i j : YHom A a b } → i == j → j == i |
| 358 | 76 sym1 {a} {b} {i} {j} eq {x} = sym eq |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
77 trans1 : {a b : YObj A } {i j k : YHom A a b} → i == j → j == k → i == k |
| 358 | 78 trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
79 o-resp-≈ : {A₁ B C : YObj A} {f g : YHom A A₁ B} {h i : YHom A B C} → |
| 189 | 80 f == g → h == i → h + f == i + g |
| 358 | 81 o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
82 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
83 SetsAop : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
84 SetsAop {_} {c₂} {_} A = |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
85 record { Obj = YObj A |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
86 ; Hom = YHom A |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
87 ; _o_ = _+_ |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
88 ; _≈_ = _==_ |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
89 ; Id = Yid A |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
90 ; isCategory = isSetsAop A |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
91 } |
|
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
92 |
| 197 | 93 -- A is Locally small |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
94 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 |
| 197 | 95 |
| 96 import Relation.Binary.PropositionalEquality | |
| 97 -- 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 ) | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
98 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
| 197 | 99 |
| 100 | |
| 101 ---- | |
| 102 -- | |
| 103 -- Object mapping in Yoneda Functor | |
| 104 -- | |
| 105 ---- | |
| 106 | |
| 107 open import Function | |
| 108 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
109 y-obj : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor (Category.op A) (Sets {c₂}) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
110 y-obj {_} {c₂} {_} A a = record { |
| 197 | 111 FObj = λ b → Hom (Category.op A) a b ; |
| 112 FMap = λ {b c : Obj A } → λ ( f : Hom A c b ) → λ (g : Hom A b a ) → (Category.op A) [ f o g ] ; | |
| 113 isFunctor = record { | |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
114 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
115 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; |
|
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
116 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
| 197 | 117 } |
| 118 } where | |
| 119 lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
120 lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL |
| 197 | 121 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ |
| 122 Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
123 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin |
| 197 | 124 Category.op A [ Category.op A [ g o f ] o x ] |
| 125 ≈↑⟨ assoc ⟩ | |
| 126 Category.op A [ g o Category.op A [ f o x ] ] | |
| 127 ≈⟨⟩ | |
| 128 ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) | |
| 129 ∎ ) | |
| 130 lemma-y-obj3 : {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 ] | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
131 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin |
| 197 | 132 Category.op A [ f o x ] |
| 133 ≈⟨ resp refl-hom eq ⟩ | |
| 134 Category.op A [ g o x ] | |
| 135 ∎ ) | |
| 136 | |
| 137 | |
| 138 ---- | |
| 139 -- | |
| 140 -- Hom mapping in Yoneda Functor | |
| 141 -- | |
| 142 ---- | |
| 143 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
144 y-tmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) → (f : Hom A a b ) → (x : Obj (Category.op A)) → |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
145 FObj (y-obj A a) x → FObj (y-obj A b ) x |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
146 y-tmap {_} {c₂} {_} A a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) |
| 197 | 147 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
148 y-map : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } → (f : Hom A a b ) → YHom A (y-obj A a) (y-obj A b) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
149 y-map {_} {c₂} {_} A {a} {b} f = record { TMap = y-tmap A a b f ; isNTrans = isNTrans1 {a} {b} f } where |
| 197 | 150 lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
151 Sets [ Sets [ FMap (y-obj A b) g o y-tmap A a b f a₁ ] ≈ |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
152 Sets [ y-tmap A a b f b₁ o FMap (y-obj A a) g ] ] |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
153 lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin |
| 197 | 154 A [ A [ f o x ] o g ] |
| 155 ≈↑⟨ assoc ⟩ | |
| 156 A [ f o A [ x o g ] ] | |
| 157 ∎ ) ) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
158 isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) (y-obj A b) (y-tmap A a b f ) |
| 197 | 159 isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } |
| 160 | |
| 161 ----- | |
| 162 -- | |
| 163 -- Yoneda Functor itself | |
| 164 -- | |
| 165 ----- | |
| 166 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
167 YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A) |
| 783 | 168 YonedaFunctor A = record { |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
169 FObj = λ a → y-obj A a |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
170 ; FMap = λ f → y-map A f |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
171 ; isFunctor = record { |
| 187 | 172 identity = identity |
| 173 ; distr = distr1 | |
| 174 ; ≈-cong = ≈-cong | |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
175 |
|
186
b2e01aa0924d
y-nat (FMap of Yoneda Functor )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
185
diff
changeset
|
176 } |
| 187 | 177 } where |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
178 ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop A [ y-map A f ≈ y-map A g ] |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
179 ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning (A) in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
180 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
181 A [ f o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
182 ≈⟨ resp refl-hom eq ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
183 A [ g o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
184 ∎ |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
185 ) ) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
186 identity : {a : Obj A} → SetsAop A [ y-map A (id1 A a) ≈ id1 (SetsAop A) (y-obj A a ) ] |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
187 identity {a} = let open ≈-Reasoning (A) in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
188 extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin |
|
188
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 ∎ |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
193 ) ) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
194 distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop A [ y-map A (A [ g o f ]) ≈ SetsAop A [ y-map A g o y-map A f ] ] |
| 191 | 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₁ ] ] ) |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
196 extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin |
|
188
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
197 A [ A [ g o f ] o h ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
198 ≈↑⟨ assoc ⟩ |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
199 A [ g o A [ f o h ] ] |
|
f4c9d7cbcbb9
Yoneda Functor Constructed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
187
diff
changeset
|
200 ∎ |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
201 ) ) |
| 184 | 202 |
| 185 | 203 |
| 190 | 204 ------ |
| 205 -- | |
| 206 -- F : A → Sets ∈ Obj SetsAop | |
| 207 -- | |
| 300 | 208 -- F(a) → Nat(h_a,F) |
| 191 | 209 -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x |
| 190 | 210 ------ |
| 187 | 211 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
212 F2Natmap : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj ( SetsAop A) } |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
213 → {x : FObj F a} → (b : Obj (Category.op A)) → Hom Sets (FObj (y-obj A a) b) (FObj F b) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
214 F2Natmap A {a} {F} {x} b = λ ( g : Hom A b a ) → ( FMap F g ) x |
| 190 | 215 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
216 F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A )} → FObj F a → Hom (SetsAop A) (y-obj A a) F |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
217 F2Nat {_} {c₂} A {a} {F} x = record { TMap = F2Natmap A {a} {F} {x} ; isNTrans = isNTrans1 } where |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
218 commute1 : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} (g : Hom A a₁ a) → |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
219 (Sets [ FMap F f o FMap F g ]) x ≡ FMap F (A [ g o f ] ) x |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
220 commute1 g = let open ≈-Reasoning (Sets) in |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
221 cong ( λ f → f x ) ( sym ( distr F ) ) |
| 191 | 222 commute : {a₁ b : Obj (Category.op A)} {f : Hom (Category.op A) a₁ b} → |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
223 Sets [ Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] ≈ Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
224 commute {a₁} {b} {f} = let open ≈-Reasoning (Sets) in |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
225 begin |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
226 Sets [ FMap F f o F2Natmap A {a} {F} {x} a₁ ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
227 ≈⟨⟩ |
|
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
228 Sets [ FMap F f o (λ ( g : Hom A a₁ a ) → ( FMap F g ) x) ] |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
229 ≈⟨ extensionality A ( λ (g : Hom A a₁ a) → commute1 {a₁} {b} {f} g ) ⟩ |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
230 Sets [ (λ ( g : Hom A b a ) → ( FMap F g ) x) o FMap (y-obj A a) f ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
231 ≈⟨⟩ |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
232 Sets [ F2Natmap A {a} {F} {x} b o FMap (y-obj A a) f ] |
|
192
d7e4b7b441be
F(a) → Nat(h_a,F) done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
191
diff
changeset
|
233 ∎ |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
234 isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) (y-obj A a) F (F2Natmap A {a} {F}) |
| 191 | 235 isNTrans1 = record { commute = λ {a₁ b f} → commute {a₁} {b} {f} } |
| 190 | 236 |
| 237 | |
| 199 | 238 -- F(a) <- Nat(h_a,F) |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
239 Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A} → {F : Obj (SetsAop A) } → Hom (SetsAop A) (y-obj A a) F → FObj F a |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
240 Nat2F A {a} {F} ha = ( TMap ha a ) (id1 A a) |
| 190 | 241 |
| 199 | 242 ---- |
| 243 -- | |
| 244 -- Prove Bijection (as routine exercise ...) | |
| 245 -- | |
| 246 ---- | |
| 247 | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
248 F2Nat→Nat2F : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (fa : FObj F a) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
249 → Nat2F A {a} {F} (F2Nat A {a} {F} fa) ≡ fa |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
250 F2Nat→Nat2F A {a} {F} fa = let open ≈-Reasoning (Sets) in cong ( λ f → f fa ) ( |
| 199 | 251 -- FMap F (Category.Category.Id A) fa ≡ fa |
| 194 | 252 begin |
| 253 ( FMap F (id1 A _ )) | |
| 254 ≈⟨ IsFunctor.identity (isFunctor F) ⟩ | |
| 255 id1 Sets (FObj F a) | |
| 256 ∎ ) | |
| 257 | |
| 258 open import Relation.Binary.PropositionalEquality | |
| 259 | |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
260 ≡-cong = Relation.Binary.PropositionalEquality.cong |
|
193
4e6f080f0107
isomorphic problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
192
diff
changeset
|
261 |
| 195 | 262 -- F : op A → Sets |
| 197 | 263 -- ha : NTrans (op A) Sets (y-obj {a}) F |
| 264 -- FMap F g o TMap ha a ≈ TMap ha b o FMap (y-obj {a}) g | |
| 195 | 265 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
266 Nat2F→F2Nat : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a : Obj A } → {F : Obj (SetsAop A)} → (ha : Hom (SetsAop A) (y-obj A a) F) |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
267 → SetsAop A [ F2Nat A {a} {F} (Nat2F A {a} {F} ha) ≈ ha ] |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
268 Nat2F→F2Nat A {a} {F} ha {b} = let open ≡-Reasoning in |
| 194 | 269 begin |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
270 TMap (F2Nat A {a} {F} (Nat2F A {a} {F} ha)) b |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
271 ≡⟨⟩ |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
272 (λ g → FMap F g (TMap ha a (Category.Category.Id A))) |
|
468
c375d8f93a2c
discrete category and product from a limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
358
diff
changeset
|
273 ≡⟨ extensionality A (λ g → ( |
| 195 | 274 begin |
| 275 FMap F g (TMap ha a (Category.Category.Id A)) | |
| 203 | 276 ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
277 TMap ha b (FMap (y-obj A a) g (Category.Category.Id A)) |
| 195 | 278 ≡⟨⟩ |
| 279 TMap ha b ( (A Category.o Category.Category.Id A) g ) | |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
280 ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ |
| 195 | 281 TMap ha b g |
| 282 ∎ | |
|
202
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
283 )) ⟩ |
|
58ee98bbb333
remove an extensionality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
199
diff
changeset
|
284 TMap ha b |
| 195 | 285 ∎ |
| 194 | 286 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
287 -- Yoneda's Lemma |
| 199 | 288 -- Yoneda Functor is full and faithfull |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
289 -- that is FMapp Yoneda is injective and surjective |
| 194 | 290 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
291 -- λ b g → (A Category.o f₁) g |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
292 YondaLemma1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a a' : Obj A } {f : FObj (FObj (YonedaFunctor A) a) a' } |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
293 → SetsAop A [ F2Nat A {a'} {FObj (YonedaFunctor A) a} f ≈ FMap (YonedaFunctor A) f ] |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
294 YondaLemma1 A {a} {a'} {f} = refl |
| 195 | 295 |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
296 -- F2Nat is bijection so FMap YonedaFunctor also ( using functional extensionality ) |
|
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
297 |
| 204 | 298 -- Full embedding of Yoneda Functor requires injective on Object, |
| 299 -- | |
| 300 -- But we cannot prove like this | |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
301 -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b |
| 783 | 302 |
| 303 open import Relation.Nullary | |
| 304 open import Data.Empty | |
| 305 | |
| 306 --YondaLemma2 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
| 307 -- (a b x : Obj A ) → (FObj (FObj (YonedaFunctor A) a) x) ≡ (FObj (FObj (YonedaFunctor A) b ) x) → a ≡ b | |
| 308 --YondaLemma2 A a bx eq = {!!} | |
| 309 | |
| 253 | 310 -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b |
| 783 | 311 |
| 312 --record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where | |
| 313 -- infixr 9 _o_ | |
| 314 -- infix 4 _≈_ | |
| 315 -- field | |
| 316 -- Obj : Set c₁ | |
| 317 -- Hom : Obj → Obj → Set c₂ | |
| 318 --YondaLemma31 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
| 319 -- (a b x : Obj A ) → Hom A a x ≡ Hom A b x → a ≡ b | |
| 320 --YondaLemma31 A a b x eq = {!!} | |
| 204 | 321 -- |
| 253 | 322 -- Instead we prove only |
| 204 | 323 -- inv ( FObj YonedaFunctor a ) ≡ a |
|
196
c040369bd6d4
give up injective on Object?
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
195
diff
changeset
|
324 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
325 inv : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : FObj (FObj (YonedaFunctor A) a) x) → Obj A |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
326 inv A {a} f = Category.cod A f |
| 203 | 327 |
|
299
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
328 YonedaLemma21 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a x : Obj A} ( f : ( FObj (FObj (YonedaFunctor A ) a) x) ) → inv A f ≡ a |
|
8c72f5284bc8
remove module parameter from yoneda functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
253
diff
changeset
|
329 YonedaLemma21 A {a} {x} f = refl |
| 203 | 330 |
| 693 | 331 open import Relation.Binary.HeterogeneousEquality |
| 332 a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B | |
| 333 a1 refl = refl | |
| 783 | 334 |
| 335 -- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
| 336 -- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b | |
| 337 -- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ? | |
| 338 | |
| 339 a2 : ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b | |
| 340 a2 a b f g eq = {!!} | |
| 341 | |
| 342 -- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} | |
| 343 -- → FObj (FObj (YonedaFunctor A ) a ) a ≅ FObj (FObj (YonedaFunctor A ) a ) b | |
| 344 -- → a ≡ b | |
| 345 -- YonedaInjective A {a} {b} eq = {!!} | |
| 346 | |
| 347 |