Mercurial > hg > Members > kono > Proof > category
annotate freyd2.agda @ 657:0d029674eb59
on going ...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Jul 2017 12:22:54 +0900 |
| parents | 18431b63893b |
| children | 9242298cffa8 |
| rev | line source |
|---|---|
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
3 open import Category.Sets renaming ( _o_ to _*_ ) |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module freyd2 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 where |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import HomReasoning |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import cat-utility |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import Relation.Binary.Core |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open import Function |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 ---------- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 -- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 -- a : Obj A |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 -- U : A → Sets |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 -- U ⋍ Hom (a,-) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 -- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
20 -- maybe this is a part of local smallness |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
21 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 |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 import Relation.Binary.PropositionalEquality |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 -- 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 ) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
27 |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 ---- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 -- |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
30 -- Hom ( a, - ) is Object mapping in Yoneda Functor |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 -- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 ---- |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 open NTrans |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 open Functor |
|
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
36 open Limit |
|
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
37 open IsLimit |
|
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
38 open import Category.Cat |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
| 616 | 40 Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) |
| 41 Yoneda {c₁} {c₂} {ℓ} A a = record { | |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 FObj = λ b → Hom A a b |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ; FMap = λ {x} {y} (f : Hom A x y ) → λ ( g : Hom A a x ) → A [ f o g ] -- f : Hom A x y → Hom Sets (Hom A a x ) (Hom A a y) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 ; isFunctor = record { |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 identity = λ {b} → extensionality A ( λ x → lemma-y-obj1 {b} x ) ; |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 distr = λ {a} {b} {c} {f} {g} → extensionality A ( λ x → lemma-y-obj2 a b c f g x ) ; |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 ≈-cong = λ eq → extensionality A ( λ x → lemma-y-obj3 x eq ) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 } |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 } where |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 lemma-y-obj1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
51 lemma-y-obj1 {b} x = let open ≈-Reasoning A in ≈-≡ A idL |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c ) → (x : Hom A a a₁ )→ |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
54 lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning A in ≈-≡ A ( begin |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 A [ A [ g o f ] o x ] |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 ≈↑⟨ assoc ⟩ |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 A [ g o A [ f o x ] ] |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 ≈⟨⟩ |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 ( λ x → A [ g o x ] ) ( ( λ x → A [ f o x ] ) x ) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 ∎ ) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 lemma-y-obj3 : {b c : Obj A} {f g : Hom A b c } → (x : Hom A a b ) → A [ f ≈ g ] → A [ f o x ] ≡ A [ g o x ] |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
62 lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning A in ≈-≡ A ( begin |
|
497
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 A [ f o x ] |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 ≈⟨ resp refl-hom eq ⟩ |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 A [ g o x ] |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 ∎ ) |
|
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 |
| 609 | 68 -- Representable U ≈ Hom(A,-) |
| 502 | 69 |
| 609 | 70 record Representable { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( U : Functor A (Sets {c₂}) ) (a : Obj A) : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁ )) where |
| 502 | 71 field |
| 72 -- FObj U x : A → Set | |
| 609 | 73 -- FMap U f = Set → Set (locally small) |
| 502 | 74 -- λ b → Hom (a,b) : A → Set |
| 75 -- λ f → Hom (a,-) = λ b → Hom a b | |
| 76 | |
| 616 | 77 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) |
| 78 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U | |
| 79 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] | |
| 609 | 80 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] |
| 608 | 81 |
| 609 | 82 open Representable |
| 608 | 83 open import freyd |
| 502 | 84 |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
85 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
86 → ( F G : Functor A B ) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
87 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
88 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
89 where open import Comma1 F G |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
90 |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
91 open SmallFullSubcategory |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
92 open Complete |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
93 open PreInitial |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
94 open HasInitialObject |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
95 open import Comma1 |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
96 open CommaObj |
| 609 | 97 open LimitPreserve |
| 608 | 98 |
| 609 | 99 -- Representable Functor U preserve limit , so K{*}↓U is complete |
| 610 | 100 -- |
| 616 | 101 -- Yoneda A b = λ a → Hom A a b : Functor A Sets |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
102 -- : Functor Sets A |
| 610 | 103 |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
104 YonedaFpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) |
| 612 | 105 (b : Obj A ) |
| 610 | 106 (Γ : Functor I A) (limita : Limit A I Γ) → |
| 616 | 107 IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
108 YonedaFpreserveLimit0 {c₁} {c₂} {ℓ} A I b Γ lim = record { |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
109 limit = λ a t → ψ a t |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
110 ; t0f=t = λ {a t i} → t0f=t0 a t i |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
111 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t |
| 610 | 112 } where |
| 616 | 113 hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) |
| 114 hat0 = LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b) | |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
115 haa0 : Obj Sets |
| 616 | 116 haa0 = FObj (Yoneda A b) (a0 lim) |
| 117 ta : (a : Obj Sets) ( x : a ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) → NTrans I A (K A I b ) Γ | |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
118 ta a x t = record { TMap = λ i → (TMap t i ) x ; isNTrans = record { commute = commute1 } } where |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
119 commute1 : {a₁ b₁ : Obj I} {f : Hom I a₁ b₁} → |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
120 A [ A [ FMap Γ f o TMap t a₁ x ] ≈ A [ TMap t b₁ x o FMap (K A I b) f ] ] |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
121 commute1 {a₁} {b₁} {f} = let open ≈-Reasoning A in begin |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
122 FMap Γ f o TMap t a₁ x |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
123 ≈⟨⟩ |
| 616 | 124 ( ( FMap (Yoneda A b ○ Γ ) f ) * TMap t a₁ ) x |
|
611
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
125 ≈⟨ ≡-≈ ( cong (λ k → k x ) (IsNTrans.commute (isNTrans t)) ) ⟩ |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
126 ( TMap t b₁ * ( FMap (K Sets I a) f ) ) x |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
127 ≈⟨⟩ |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
128 ( TMap t b₁ * id1 Sets a ) x |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
129 ≈⟨⟩ |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
130 TMap t b₁ x |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
131 ≈↑⟨ idR ⟩ |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
132 TMap t b₁ x o id1 A b |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
133 ≈⟨⟩ |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
134 TMap t b₁ x o FMap (K A I b) f |
|
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
135 ∎ |
| 616 | 136 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) |
| 137 → Hom Sets X (FObj (Yoneda A b) (a0 lim)) | |
| 138 ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) | |
| 139 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) | |
| 140 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] | |
| 612 | 141 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
| 616 | 142 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x |
| 612 | 143 ≈⟨⟩ |
| 616 | 144 FMap (Yoneda A b) ( TMap (t0 lim) i) (FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b )) |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
145 ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] |
| 613 | 146 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) |
| 147 ≈⟨ cdr idR ⟩ | |
| 148 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) | |
| 149 ≈⟨ t0f=t (isLimit lim) ⟩ | |
| 150 TMap (ta a x t) i | |
| 151 ≈⟨⟩ | |
| 612 | 152 TMap t i x |
| 153 ∎ )) | |
| 616 | 154 limit-uniqueness0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)} {f : Hom Sets a (FObj (Yoneda A b) (a0 lim))} → |
| 155 ({i : Obj I} → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o f ] ≈ TMap t i ]) → | |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
156 Sets [ ψ a t ≈ f ] |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
157 limit-uniqueness0 {a} {t} {f} t0f=t = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
158 ψ a t x |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
159 ≈⟨⟩ |
| 616 | 160 FMap (Yoneda A b) (limit (isLimit lim) b (ta a x t )) (id1 A b ) |
|
614
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
161 ≈⟨⟩ |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
162 limit (isLimit lim) b (ta a x t ) o id1 A b |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
163 ≈⟨ idR ⟩ |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
164 limit (isLimit lim) b (ta a x t ) |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
165 ≈⟨ limit-uniqueness (isLimit lim) ( λ {i} → ≡-≈ ( cong ( λ g → g x )( t0f=t {i} ))) ⟩ |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
166 f x |
|
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
167 ∎ )) |
| 610 | 168 |
| 609 | 169 |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
170 YonedaFpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) |
| 616 | 171 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
172 YonedaFpreserveLimit A I b = record { |
|
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
173 preserve = λ Γ lim → YonedaFpreserveLimit0 A I b Γ lim |
| 610 | 174 } |
| 609 | 175 |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
176 |
| 608 | 177 -- K{*}↓U has preinitial full subcategory if U is representable |
| 609 | 178 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) |
| 608 | 179 |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
180 open CommaHom |
|
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
181 |
| 627 | 182 data * {c : Level} : Set c where |
| 183 OneObj : * | |
| 184 | |
| 609 | 185 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 608 | 186 (a : Obj A ) |
| 628 | 187 → HasInitialObject ( K (Sets) A * ↓ (Yoneda A a) ) ( record { obj = a ; hom = λ x → id1 A a } ) |
| 621 | 188 KUhasInitialObj {c₁} {c₂} {ℓ} A a = record { |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
189 initial = λ b → initial0 b |
| 636 | 190 ; uniqueness = λ f → unique f |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
191 } where |
| 621 | 192 commaCat : Category (c₂ ⊔ c₁) c₂ ℓ |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
193 commaCat = K Sets A * ↓ Yoneda A a |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
194 initObj : Obj (K Sets A * ↓ Yoneda A a) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
195 initObj = record { obj = a ; hom = λ x → id1 A a } |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
196 comm2 : (b : Obj commaCat) ( x : * ) → ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) x ≡ hom b x |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
197 comm2 b OneObj = let open ≈-Reasoning A in ≈-≡ A ( begin |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
198 ( Sets [ FMap (Yoneda A a) (hom b OneObj) o (λ x₁ → id1 A a) ] ) OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
199 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
200 FMap (Yoneda A a) (hom b OneObj) (id1 A a) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
201 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
202 hom b OneObj o id1 A a |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
203 ≈⟨ idR ⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
204 hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
205 ∎ ) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
206 comm1 : (b : Obj commaCat) → Sets [ Sets [ FMap (Yoneda A a) (hom b OneObj) o hom initObj ] ≈ Sets [ hom b o FMap (K Sets A *) (hom b OneObj) ] ] |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
207 comm1 b = let open ≈-Reasoning Sets in begin |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
208 FMap (Yoneda A a) (hom b OneObj) o ( λ x → id1 A a ) |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
209 ≈⟨ extensionality A ( λ x → comm2 b x ) ⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
210 hom b |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
211 ≈⟨⟩ |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
212 hom b o FMap (K Sets A *) (hom b OneObj) |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
213 ∎ |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
214 initial0 : (b : Obj commaCat) → |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
215 Hom commaCat initObj b |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
216 initial0 b = record { |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
217 arrow = hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
218 ; comm = comm1 b } |
| 625 | 219 -- what is comm f ? |
| 220 comm-f : (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) | |
| 221 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] | |
| 222 ≈ Sets [ hom b o FMap (K Sets A *) (arrow f) ] ] | |
| 223 comm-f b f = comm f | |
| 636 | 224 unique : {b : Obj (K Sets A * ↓ Yoneda A a)} (f : Hom (K Sets A * ↓ Yoneda A a) initObj b) |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
225 → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ] |
| 636 | 226 unique {b} f = let open ≈-Reasoning A in begin |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
227 arrow f |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
228 ≈↑⟨ idR ⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
229 arrow f o id1 A a |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
230 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
231 ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) |
| 625 | 232 ≈⟨⟩ |
| 233 ( Sets [ FMap (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj | |
| 234 ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩ | |
|
624
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
235 ( Sets [ hom b o FMap (K Sets A *) (arrow f) ] ) OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
236 ≈⟨⟩ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
237 hom b OneObj |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
238 ∎ |
|
9b9bc1e076f3
introduce one element set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
623
diff
changeset
|
239 |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
240 |
|
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
241 |
|
644
8e35703ef116
representability theorem done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
643
diff
changeset
|
242 -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable |
|
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
243 |
|
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
244 open SmallFullSubcategory |
|
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
245 open PreInitial |
| 626 | 246 |
| 638 | 247 -- if U preserve limit, K{*}↓U has initial object from freyd.agda |
| 248 | |
| 626 | 249 ≡-cong = Relation.Binary.PropositionalEquality.cong |
| 250 | |
| 638 | 251 |
| 252 ub : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) | |
| 253 → Hom Sets (FObj (K Sets A *) b) (FObj U b) | |
| 254 ub A U b x OneObj = x | |
| 255 ob : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) )(b : Obj A) (x : FObj U b ) | |
| 256 → Obj ( K Sets A * ↓ U) | |
| 257 ob A U b x = record { obj = b ; hom = ub A U b x} | |
| 258 fArrow : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (U : Functor A (Sets {c₂}) ) {a b : Obj A} (f : Hom A a b) (x : FObj U a ) | |
| 259 → Hom ( K Sets A * ↓ U) ( ob A U a x ) (ob A U b (FMap U f x) ) | |
| 260 fArrow A U {a} {b} f x = record { arrow = f ; comm = fArrowComm a b f x } | |
| 261 where | |
| 262 fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub A U a x y ) ≡ ub A U b (FMap U f x) y | |
| 263 fArrowComm1 a b f x OneObj = refl | |
| 264 fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → | |
| 265 Sets [ Sets [ FMap U f o hom (ob A U a x) ] ≈ Sets [ hom (ob A U b (FMap U f x)) o FMap (K Sets A *) f ] ] | |
| 266 fArrowComm a b f x = extensionality Sets ( λ y → begin | |
| 267 ( Sets [ FMap U f o hom (ob A U a x) ] ) y | |
| 268 ≡⟨⟩ | |
| 269 FMap U f ( hom (ob A U a x) y ) | |
| 270 ≡⟨⟩ | |
| 271 FMap U f ( ub A U a x y ) | |
| 272 ≡⟨ fArrowComm1 a b f x y ⟩ | |
| 273 ub A U b (FMap U f x) y | |
| 274 ≡⟨⟩ | |
| 275 hom (ob A U b (FMap U f x)) y | |
| 276 ∎ ) where | |
| 277 open import Relation.Binary.PropositionalEquality | |
| 278 open ≡-Reasoning | |
| 279 | |
|
635
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
280 |
|
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
281 -- if K{*}↓U has initial Obj, U is representable |
|
f7cc0ec00e05
introduce U preserving
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
634
diff
changeset
|
282 |
| 636 | 283 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 626 | 284 (U : Functor A (Sets {c₂}) ) |
| 636 | 285 ( i : Obj ( K (Sets) A * ↓ U) ) |
| 286 (In : HasInitialObject ( K (Sets) A * ↓ U) i ) | |
| 287 → Representable A U (obj i) | |
| 288 UisRepresentable A U i In = record { | |
| 627 | 289 repr→ = record { TMap = tmap1 ; isNTrans = record { commute = comm1 } } |
| 626 | 290 ; repr← = record { TMap = tmap2 ; isNTrans = record { commute = comm2 } } |
| 638 | 291 ; reprId→ = iso→ |
| 292 ; reprId← = iso← | |
| 626 | 293 } where |
| 638 | 294 comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → |
| 295 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y | |
| 296 ≡ (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y | |
| 297 comm11 a b f y = begin | |
| 298 ( Sets [ FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In (ob A U a x))) ] ) y | |
| 631 | 299 ≡⟨⟩ |
| 638 | 300 A [ f o arrow (initial In (ob A U a y)) ] |
| 631 | 301 ≡⟨⟩ |
| 638 | 302 A [ arrow ( fArrow A U f y ) o arrow (initial In (ob A U a y)) ] |
| 303 ≡⟨ ≈-≡ A ( uniqueness In {ob A U b (FMap U f y) } (( K Sets A * ↓ U) [ fArrow A U f y o initial In (ob A U a y)] ) ) ⟩ | |
| 304 arrow (initial In (ob A U b (FMap U f y) )) | |
| 629 | 305 ≡⟨⟩ |
| 638 | 306 (Sets [ ( λ x → arrow (initial In (ob A U b x))) o FMap U f ] ) y |
| 629 | 307 ∎ where |
| 308 open import Relation.Binary.PropositionalEquality | |
| 309 open ≡-Reasoning | |
| 636 | 310 tmap1 : (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj i)) b) |
| 638 | 311 tmap1 b x = arrow ( initial In (ob A U b x ) ) |
| 636 | 312 comm1 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap (Yoneda A (obj i)) f o tmap1 a ] ≈ Sets [ tmap1 b o FMap U f ] ] |
| 626 | 313 comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin |
| 636 | 314 FMap (Yoneda A (obj i)) f o tmap1 a |
| 629 | 315 ≈⟨⟩ |
| 638 | 316 FMap (Yoneda A (obj i)) f o ( λ x → arrow (initial In ( ob A U a x ))) |
| 629 | 317 ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩ |
| 638 | 318 ( λ x → arrow (initial In (ob A U b x))) o FMap U f |
| 629 | 319 ≈⟨⟩ |
| 626 | 320 tmap1 b o FMap U f |
| 321 ∎ | |
| 636 | 322 comm21 : (a b : Obj A) (f : Hom A a b) ( y : Hom A (obj i) a ) → |
| 323 (Sets [ FMap U f o (λ x → FMap U x (hom i OneObj))] ) y ≡ | |
| 324 (Sets [ ( λ x → (FMap U x ) (hom i OneObj)) o (λ x → A [ f o x ] ) ] ) y | |
| 626 | 325 comm21 a b f y = begin |
| 636 | 326 FMap U f ( FMap U y (hom i OneObj)) |
| 327 ≡⟨ ≡-cong ( λ k → k (hom i OneObj)) ( sym ( IsFunctor.distr (isFunctor U ) ) ) ⟩ | |
| 328 (FMap U (A [ f o y ] ) ) (hom i OneObj) | |
| 626 | 329 ∎ where |
| 330 open import Relation.Binary.PropositionalEquality | |
| 331 open ≡-Reasoning | |
| 636 | 332 tmap2 : (b : Obj A) → Hom Sets (FObj (Yoneda A (obj i)) b) (FObj U b) |
| 333 tmap2 b x = ( FMap U x ) ( hom i OneObj ) | |
| 626 | 334 comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈ |
| 636 | 335 Sets [ tmap2 b o FMap (Yoneda A (obj i)) f ] ] |
| 626 | 336 comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin |
| 337 FMap U f o tmap2 a | |
| 338 ≈⟨⟩ | |
| 636 | 339 FMap U f o ( λ x → ( FMap U x ) ( hom i OneObj ) ) |
| 626 | 340 ≈⟨ extensionality Sets ( λ y → comm21 a b f y ) ⟩ |
| 636 | 341 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o ( λ x → A [ f o x ] ) |
| 342 ≈⟨⟩ | |
| 343 ( λ x → ( FMap U x ) ( hom i OneObj ) ) o FMap (Yoneda A (obj i)) f | |
| 344 ≈⟨⟩ | |
| 345 tmap2 b o FMap (Yoneda A (obj i)) f | |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
346 ∎ |
|
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
347 iso0 : ( x : Obj A) ( y : Hom A (obj i ) x ) ( z : * ) |
| 638 | 348 → ( Sets [ FMap U y o hom i ] ) z ≡ ( Sets [ ub A U x (FMap U y (hom i OneObj)) o FMap (K Sets A *) y ] ) z |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
349 iso0 x y OneObj = refl |
| 636 | 350 iso→ : {x : Obj A} → Sets [ Sets [ tmap1 x o tmap2 x ] ≈ id1 Sets (FObj (Yoneda A (obj i)) x) ] |
| 351 iso→ {x} = let open ≈-Reasoning A in extensionality Sets ( λ ( y : Hom A (obj i ) x ) → ≈-≡ A ( begin | |
| 352 ( Sets [ tmap1 x o tmap2 x ] ) y | |
| 626 | 353 ≈⟨⟩ |
| 638 | 354 arrow ( initial In (ob A U x (( FMap U y ) ( hom i OneObj ) ))) |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
355 ≈↑⟨ uniqueness In (record { arrow = y ; comm = extensionality Sets ( λ (z : * ) → iso0 x y z ) } ) ⟩ |
| 636 | 356 y |
| 357 ∎ )) | |
| 358 iso← : {x : Obj A} → Sets [ Sets [ tmap2 x o tmap1 x ] ≈ id1 Sets (FObj U x) ] | |
| 359 iso← {x} = extensionality Sets ( λ (y : FObj U x ) → ( begin | |
| 360 ( Sets [ tmap2 x o tmap1 x ] ) y | |
| 361 ≡⟨⟩ | |
| 638 | 362 ( FMap U ( arrow ( initial In (ob A U x y ) )) ) ( hom i OneObj ) |
| 363 ≡⟨ ≡-cong (λ k → k OneObj) ( comm ( initial In (ob A U x y ) )) ⟩ | |
| 364 hom (ob A U x y) OneObj | |
|
637
946ea019a2e7
if K{*}↓U has initial Obj, U is representable done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
636
diff
changeset
|
365 ≡⟨⟩ |
| 636 | 366 y |
| 367 ∎ ) ) where | |
| 368 open import Relation.Binary.PropositionalEquality | |
| 369 open ≡-Reasoning | |
| 645 | 370 |
| 647 | 371 ------------- |
| 372 -- Adjoint Functor Theorem | |
| 373 -- | |
| 374 | |
| 648 | 375 module Adjoint-Functor {c₁ c₂ ℓ : Level} (A B : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) ( comp : Complete A I ) |
| 376 (U : Functor A B ) | |
| 377 (SFS : (b : Obj B) → SmallFullSubcategory ((K B A b) ↓ U) ) | |
| 650 | 378 (PI : (b : Obj B) → PreInitial (K B A b ↓ U) (SFSF (SFS b))) |
| 379 ( i : (b : Obj B) → Obj ( K B A b ↓ U) ) | |
| 380 (In : (b : Obj B) → HasInitialObject ( K B A b ↓ U) (i b) ) | |
| 648 | 381 (LP : LimitPreserve A I B U ) where |
| 382 | |
| 649 | 383 tmap-η : (y : Obj B) → Hom B y (FObj U (obj (i y))) |
| 384 tmap-η y = hom (i y) | |
| 648 | 385 |
| 652 | 386 sobj : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaObj (K B A a) U |
| 387 sobj {a} {b} f = record {obj = b; hom = f } | |
| 388 solution : {a : Obj B} {b : Obj A} → ( f : Hom B a (FObj U b) ) → CommaHom (K B A a) U (i a) (sobj f) | |
| 389 solution {a} {b} f = initial (In a) (sobj f) | |
| 647 | 390 |
| 654 | 391 ηf : (a b : Obj B) → ( f : Hom B a b ) → Obj ( K B A a ↓ U) |
| 392 ηf a b f = sobj ( B [ tmap-η b o f ] ) | |
| 393 | |
| 653 | 394 univ : {a : Obj B} {b : Obj A} → (f : Hom B a (FObj U b)) |
| 652 | 395 → B [ B [ FMap U (arrow (solution f)) o tmap-η a ] ≈ f ] |
| 653 | 396 univ {a} {b} f = let open ≈-Reasoning B in begin |
| 397 FMap U (arrow (solution f)) o tmap-η a | |
| 398 ≈⟨ comm (initial (In a) (sobj f)) ⟩ | |
| 399 hom (sobj f) o FMap (K B A a) (arrow (initial (In a) (sobj f))) | |
| 400 ≈⟨ idR ⟩ | |
| 401 f | |
| 402 ∎ | |
| 652 | 403 |
| 654 | 404 unique : {a : Obj B} { b : Obj A } → { f : Hom B a (FObj U b) } → { g : Hom A (obj (i a)) b} → |
| 405 B [ B [ FMap U g o tmap-η a ] ≈ f ] → A [ arrow (solution f) ≈ g ] | |
| 406 unique {a} {b} {f} {g} ugη=f = let open ≈-Reasoning A in begin | |
| 407 arrow (solution f) | |
| 408 ≈↑⟨ ≡-≈ ( cong (λ k → arrow (solution k)) ( ≈-≡ B ugη=f )) ⟩ | |
| 409 arrow (solution (B [ FMap U g o tmap-η a ] )) | |
| 410 ≈↑⟨ uniqueness (In a) (record { arrow = g ; comm = comm1 }) ⟩ | |
| 411 g | |
| 412 ∎ where | |
| 413 comm1 : B [ B [ FMap U g o hom (i a) ] ≈ B [ B [ FMap U g o tmap-η a ] o FMap (K B A a) g ] ] | |
| 414 comm1 = let open ≈-Reasoning B in sym idR | |
| 645 | 415 |
| 655 | 416 UM : UniversalMapping B A U (λ b → obj (i b)) (tmap-η) |
| 417 UM = record { | |
| 418 _* = λ f → arrow (solution f) ; | |
| 419 isUniversalMapping = record { | |
| 420 universalMapping = λ {a} {b} {f} → univ f ; | |
| 421 uniquness = unique | |
| 422 }} | |
| 423 | |
| 649 | 424 F : Functor B A |
| 425 F = record { | |
| 647 | 426 FObj = λ b → obj (i b) |
| 652 | 427 ; FMap = λ {x} {y} (f : Hom B x y ) → arrow (solution ( B [ tmap-η y o f ] )) |
| 649 | 428 ; isFunctor = record { |
| 650 | 429 identity = identity1 |
| 430 ; distr = distr1 | |
| 431 ; ≈-cong = cong1 | |
| 646 | 432 } |
| 649 | 433 } where |
| 651 | 434 id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ] |
| 435 ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ] | |
| 436 id1comm {a} = let open ≈-Reasoning B in begin | |
| 437 FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) | |
| 438 ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩ | |
| 439 hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) | |
| 440 ≈⟨ idR ⟩ | |
| 441 hom (ηf a a (id1 B a)) | |
| 442 ≈⟨⟩ | |
| 443 hom (i a) o id1 B a | |
| 444 ≈⟨ idR ⟩ | |
| 445 hom (i a) | |
| 446 ≈↑⟨ idR ⟩ | |
| 447 hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) | |
| 448 ∎ | |
| 650 | 449 identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ] |
| 651 | 450 identity1 {a} = let open ≈-Reasoning A in begin |
| 451 arrow (initial (In a) (ηf a a (id1 B a))) | |
| 452 ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩ | |
| 453 arrow (initial (In a) (i a)) | |
| 454 ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩ | |
| 455 id1 A (obj (i a)) | |
| 456 ∎ | |
| 648 | 457 distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → |
| 650 | 458 A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈ |
| 459 A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ] | |
| 656 | 460 distr1 {a} {b} {c} {f} {g} = unique ( |
| 461 let open ≈-Reasoning B in begin | |
| 462 FMap U (A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ) o tmap-η a | |
| 463 ≈⟨ car (IsFunctor.distr (isFunctor U )) ⟩ | |
| 464 ( FMap U (arrow (initial (In b) (ηf b c g))) o FMap U (arrow (initial (In a) (ηf a b f))) ) | |
| 465 o tmap-η a | |
| 466 ≈↑⟨ assoc ⟩ | |
| 467 FMap U (arrow (initial (In b) (ηf b c g))) o | |
| 468 (FMap U (arrow (initial (In a) (ηf a b f))) o tmap-η a ) | |
| 469 ≈⟨ cdr (univ ( tmap-η b o f )) ⟩ | |
| 470 FMap U (arrow (initial (In b) (ηf b c g))) o ( tmap-η b o f ) | |
| 471 ≈⟨ assoc ⟩ | |
| 472 (FMap U (arrow (initial (In b) (ηf b c g))) o tmap-η b ) o f | |
| 473 ≈⟨ car ( univ (tmap-η c o g )) ⟩ | |
| 474 (tmap-η c o g ) o f | |
| 475 ≈↑⟨ assoc ⟩ | |
| 476 tmap-η c o ( g o f ) | |
| 477 ∎ | |
| 478 ) | |
| 648 | 479 cong1 : {a : Obj B} {b : Obj B} {f g : Hom B a b} → |
| 650 | 480 B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ] |
| 656 | 481 cong1 {a} {b} {f} {g} f≈g = unique ( |
| 482 let open ≈-Reasoning B in begin | |
| 483 FMap U (arrow (initial (In a) (ηf a b g))) o tmap-η a | |
| 484 ≈⟨ univ ( tmap-η b o g ) ⟩ | |
| 485 tmap-η b o g | |
| 486 ≈↑⟨ cdr f≈g ⟩ | |
| 487 tmap-η b o f | |
| 488 ∎ | |
| 489 ) | |
| 645 | 490 |
| 656 | 491 nat-ε : NTrans A A (F ○ U) identityFunctor |
| 649 | 492 nat-ε = record { |
| 652 | 493 TMap = λ x → arrow ( solution (id1 B (FObj U x))) |
| 650 | 494 ; isNTrans = record { commute = comm1 } } where |
| 657 | 495 lemma-nat1 : {a b : Obj A} {f : Hom A a b} → |
| 496 B [ B [ FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) | |
| 497 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) ] | |
| 498 ≈ B [ FMap U f o id1 B (FObj U a) ] ] | |
| 499 lemma-nat1 {a} {b} {f} = let open ≈-Reasoning B in begin | |
| 500 FMap U (A [ FMap (identityFunctor {_} {_} {_} {A}) f o arrow (initial (In (FObj U a)) | |
| 501 (record { obj = a ; hom = id1 B (FObj U a) })) ] ) o tmap-η (FObj U a) | |
| 502 ≈⟨ car (distr U) ⟩ | |
| 503 ( FMap U (FMap (identityFunctor {_} {_} {_} {A}) f) o FMap U (arrow (initial (In (FObj U a)) | |
| 504 (record { obj = a ; hom = id1 B (FObj U a) })))) o (tmap-η (FObj U a)) | |
| 505 ≈⟨ {!!} ⟩ | |
| 506 FMap U f | |
| 507 ≈↑⟨ idR ⟩ | |
| 508 FMap U f o id1 B (FObj U a) | |
| 509 ∎ | |
| 510 lemma-nat2 : {a b : Obj A} {f : Hom A a b} → | |
| 511 B [ B [ FMap U (A [ arrow (initial (In (FObj U b)) | |
| 512 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) ] | |
| 513 ≈ B [ FMap U f o id1 B (FObj U a) ] ] | |
| 514 lemma-nat2 {a} {b} {f} = let open ≈-Reasoning B in begin | |
| 515 FMap U (A [ arrow (initial (In (FObj U b)) | |
| 516 (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ) o tmap-η (FObj U a) | |
| 517 ≈⟨ {!!} ⟩ | |
| 518 FMap U f o id1 B (FObj U a) | |
| 519 ∎ | |
| 648 | 520 comm1 : {a b : Obj A} {f : Hom A a b} → |
| 649 | 521 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o |
| 648 | 522 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ] |
| 650 | 523 ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ] |
| 656 | 524 comm1 {a} {b} {f} = let open ≈-Reasoning A in begin |
| 525 FMap (identityFunctor {_} {_} {_} {A}) f o | |
| 526 arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) | |
| 657 | 527 ≈↑⟨ unique lemma-nat1 ⟩ |
| 656 | 528 arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) |
| 657 | 529 ≈⟨ unique lemma-nat2 ⟩ |
| 656 | 530 arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f |
| 531 ∎ | |
| 645 | 532 |
| 649 | 533 nat-η : NTrans B B identityFunctor (U ○ F) |
| 534 nat-η = record { TMap = λ y → tmap-η y ; isNTrans = record { commute = comm1 } } where | |
| 651 | 535 comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ] |
| 647 | 536 comm1 {a} {b} {f} = let open ≈-Reasoning B in begin |
| 649 | 537 FMap (U ○ F) f o tmap-η a |
| 647 | 538 ≈⟨⟩ |
| 650 | 539 FMap U ( arrow ( initial (In a) (ηf a b f ))) o hom ( i a ) |
| 540 ≈⟨ comm ( initial (In a) (ηf a b f)) ⟩ | |
| 541 ( tmap-η b o f ) o FMap (K B A a) (arrow (initial (In a) (ηf a b f))) | |
| 647 | 542 ≈⟨ idR ⟩ |
| 543 hom (i b ) o f | |
| 544 ≈⟨⟩ | |
| 649 | 545 tmap-η b o f |
| 647 | 546 ∎ |
| 645 | 547 |
| 649 | 548 FisLeftAdjoint : Adjunction B A U F nat-η nat-ε |
| 549 FisLeftAdjoint = record { isAdjunction = record { | |
| 650 | 550 adjoint1 = adjoint1 |
| 551 ; adjoint2 = adjoint2 | |
| 646 | 552 } } where |
| 649 | 553 adjoint1 : {b : Obj A} → B [ B [ FMap U (TMap nat-ε b) o TMap nat-η (FObj U b) ] ≈ id1 B (FObj U b) ] |
| 648 | 554 adjoint1 = {!!} |
| 649 | 555 adjoint2 : {a : Obj B} → A [ A [ TMap nat-ε (FObj F a) o FMap F (TMap nat-η a) ] ≈ id1 A (FObj F a) ] |
| 648 | 556 adjoint2 = {!!} |