Mercurial > hg > Members > kono > Proof > category
annotate freyd2.agda @ 617:34540494fdcf
initital obj uniquness done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jun 2017 18:49:21 +0900 |
parents | 7011165c118e |
children | 23ff2464f7ad |
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 |
608 | 20 ---- |
21 -- C is locally small i.e. Hom C i j is a set c₁ | |
22 -- | |
23 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) | |
24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
25 field | |
26 hom→ : {i j : Obj C } → Hom C i j → I | |
27 hom← : {i j : Obj C } → ( f : I ) → Hom C i j | |
28 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f | |
29 | |
30 open Small | |
31 | |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
32 -- 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
|
33 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
|
34 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 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
|
36 -- 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
|
37 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
|
38 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 ---- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 -- |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
42 -- 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
|
43 -- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 ---- |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 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
|
47 open Functor |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
48 open Limit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
49 open IsLimit |
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
50 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
|
51 |
616 | 52 Yoneda : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a : Obj A) → Functor A (Sets {c₂}) |
53 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
|
54 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
|
55 ; 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
|
56 ; 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
|
57 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
|
58 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
|
59 ≈-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
|
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 } where |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 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
|
63 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
|
64 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
|
65 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
|
66 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
|
67 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
|
68 ≈↑⟨ assoc ⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 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
|
70 ≈⟨⟩ |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 ( λ 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
|
72 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 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
|
74 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
|
75 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
|
76 ≈⟨ 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
|
77 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
|
78 ∎ ) |
e8b85a05a6b2
add if U is iso to representable functor then preserve limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 |
609 | 80 -- Representable U ≈ Hom(A,-) |
502 | 81 |
609 | 82 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 | 83 field |
84 -- FObj U x : A → Set | |
609 | 85 -- FMap U f = Set → Set (locally small) |
502 | 86 -- λ b → Hom (a,b) : A → Set |
87 -- λ f → Hom (a,-) = λ b → Hom a b | |
88 | |
616 | 89 repr→ : NTrans A (Sets {c₂}) U (Yoneda A a ) |
90 repr← : NTrans A (Sets {c₂}) (Yoneda A a) U | |
91 reprId→ : {x : Obj A} → Sets [ Sets [ TMap repr→ x o TMap repr← x ] ≈ id1 (Sets {c₂}) (FObj (Yoneda A a) x )] | |
609 | 92 reprId← : {x : Obj A} → Sets [ Sets [ TMap repr← x o TMap repr→ x ] ≈ id1 (Sets {c₂}) (FObj U x)] |
608 | 93 |
609 | 94 open Representable |
608 | 95 open import freyd |
502 | 96 |
608 | 97 _↓_ : { c₁ c₂ ℓ : Level} { c₁' c₂' ℓ' : Level} { A : Category c₁ c₂ ℓ } { B : Category c₁' c₂' ℓ' } |
98 → ( F G : Functor A B ) | |
99 → Category (c₂' ⊔ c₁) (ℓ' ⊔ c₂) ℓ | |
100 _↓_ { c₁} {c₂} {ℓ} {c₁'} {c₂'} {ℓ'} { A } { B } F G = CommaCategory | |
101 where open import Comma1 F G | |
498
c981a2f0642f
UpreseveLimit detailing
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
497
diff
changeset
|
102 |
608 | 103 open import freyd |
104 open SmallFullSubcategory | |
105 open Complete | |
106 open PreInitial | |
609 | 107 open HasInitialObject |
108 open import Comma1 | |
109 open CommaObj | |
110 open LimitPreserve | |
608 | 111 |
609 | 112 -- Representable Functor U preserve limit , so K{*}↓U is complete |
610 | 113 -- |
616 | 114 -- 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
|
115 -- : Functor Sets A |
610 | 116 |
117 UpreserveLimit0 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) | |
612 | 118 (b : Obj A ) |
610 | 119 (Γ : Functor I A) (limita : Limit A I Γ) → |
616 | 120 IsLimit Sets I (Yoneda A b ○ Γ) (FObj (Yoneda A b) (a0 limita)) (LimitNat A I Sets Γ (a0 limita) (t0 limita) (Yoneda A b)) |
612 | 121 UpreserveLimit0 {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
|
122 limit = λ a t → ψ a t |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
123 ; 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
|
124 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t |
610 | 125 } where |
616 | 126 hat0 : NTrans I Sets (K Sets I (FObj (Yoneda A b) (a0 lim))) (Yoneda A b ○ Γ) |
127 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
|
128 haa0 : Obj Sets |
616 | 129 haa0 = FObj (Yoneda A b) (a0 lim) |
130 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
|
131 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
|
132 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
|
133 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
|
134 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
|
135 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
|
136 ≈⟨⟩ |
616 | 137 ( ( 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
|
138 ≈⟨ ≡-≈ ( 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
|
139 ( 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
|
140 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
141 ( 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
|
142 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
143 TMap t b₁ x |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
144 ≈↑⟨ idR ⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
145 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
|
146 ≈⟨⟩ |
b1b5c6b4c570
natural transformation in representable functor
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
610
diff
changeset
|
147 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
|
148 ∎ |
616 | 149 ψ : (X : Obj Sets) ( t : NTrans I Sets (K Sets I X) (Yoneda A b ○ Γ)) |
150 → Hom Sets X (FObj (Yoneda A b) (a0 lim)) | |
151 ψ X t x = FMap (Yoneda A b) (limit (isLimit lim) b (ta X x t )) (id1 A b ) | |
152 t0f=t0 : (a : Obj Sets ) ( t : NTrans I Sets (K Sets I a) (Yoneda A b ○ Γ)) (i : Obj I) | |
153 → Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ≈ TMap t i ] | |
612 | 154 t0f=t0 a t i = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin |
616 | 155 ( Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) (Yoneda A b)) i o ψ a t ] ) x |
612 | 156 ≈⟨⟩ |
616 | 157 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
|
158 ≈⟨⟩ -- FMap (Hom A b ) f g = A [ f o g ] |
613 | 159 TMap (t0 lim) i o (limit (isLimit lim) b (ta a x t ) o id1 A b ) |
160 ≈⟨ cdr idR ⟩ | |
161 TMap (t0 lim) i o limit (isLimit lim) b (ta a x t ) | |
162 ≈⟨ t0f=t (isLimit lim) ⟩ | |
163 TMap (ta a x t) i | |
164 ≈⟨⟩ | |
612 | 165 TMap t i x |
166 ∎ )) | |
616 | 167 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))} → |
168 ({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
|
169 Sets [ ψ a t ≈ f ] |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
170 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
|
171 ψ a t x |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
172 ≈⟨⟩ |
616 | 173 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
|
174 ≈⟨⟩ |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
175 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
|
176 ≈⟨ idR ⟩ |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
177 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
|
178 ≈⟨ 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
|
179 f x |
e6be03d94284
Representational Functor preserve limit done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
613
diff
changeset
|
180 ∎ )) |
610 | 181 |
609 | 182 |
183 UpreserveLimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (I : Category c₁ c₂ ℓ) | |
616 | 184 (b : Obj A ) → LimitPreserve A I Sets (Yoneda A b) |
612 | 185 UpreserveLimit A I b = record { |
186 preserve = λ Γ lim → UpreserveLimit0 A I b Γ lim | |
610 | 187 } |
609 | 188 |
608 | 189 -- K{*}↓U has preinitial full subcategory if U is representable |
609 | 190 -- if U is representable, K{*}↓U has initial Object ( so it has preinitial full subcategory ) |
608 | 191 |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
192 open CommaHom |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
193 |
609 | 194 KUhasInitialObj : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
608 | 195 (a : Obj A ) |
616 | 196 → HasInitialObject {c₁} {c₂} {ℓ} ( K (Sets) A (FObj (Yoneda A a) a) ↓ (Yoneda A a) ) ( record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) } ) |
197 KUhasInitialObj A a = record { | |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
198 initial = λ b → initial0 b |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
199 ; uniqueness = λ b f → unique b f |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
200 } where |
616 | 201 initial0com1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x : FObj (Yoneda A a) a ) |
202 → FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x | |
203 initial0com1 b x = let open ≈-Reasoning A in ≈-≡ A ( begin | |
204 FMap (Yoneda A a) (hom b (id1 A a)) x | |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
205 ≈⟨⟩ |
616 | 206 hom b (id1 A a ) o x |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
207 ≈⟨ {!!} ⟩ |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
208 hom b (id1 A a o x ) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
209 ≈⟨ ≡-≈ ( cong (λ k → hom b k ) ( ≈-≡ A idL ) ) ⟩ |
616 | 210 hom b x |
211 ∎ ) | |
212 initial0com : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → | |
213 Sets [ Sets [ FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) ] ≈ | |
214 Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) ] ] | |
215 initial0com b = let open ≈-Reasoning Sets in begin | |
216 FMap (Yoneda A a) (hom b (id1 A a)) o id1 Sets (FObj (Yoneda A a) a) | |
217 ≈⟨⟩ | |
218 FMap (Yoneda A a) (hom b (id1 A a)) | |
219 ≈⟨ extensionality A ( λ x → initial0com1 b x ) ⟩ | |
220 hom b | |
221 ≈⟨⟩ | |
222 hom b o id1 Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) | |
223 ≈⟨⟩ | |
224 hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (hom b (id1 A a)) | |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
225 ∎ |
616 | 226 initial0 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → |
227 Hom ((K Sets A (FObj (Yoneda A a) a)) ↓ (Yoneda A a)) | |
228 (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b | |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
229 initial0 b = record { |
616 | 230 arrow = hom b (id1 A a) |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
231 ; comm = initial0com b } |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
232 comm-f : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
233 (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
234 → Sets [ Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
235 ≈ Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ] |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
236 comm-f b f = comm f |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
237 unique : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a)) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
238 (f : Hom (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) (record { obj = a ; hom = id1 Sets (FObj (Yoneda A a) a) }) b) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
239 → (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) [ f ≈ initial0 b ] |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
240 unique b f = let open ≈-Reasoning A in begin |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
241 arrow f |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
242 ≈↑⟨ idR ⟩ |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
243 arrow f o id1 A a |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
244 ≈⟨⟩ |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
245 ( Sets [ FMap (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a) ] ) (id1 A a) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
246 ≈⟨ ≡-≈ ( cong (λ k → k (id1 A a)) (comm f ) ) ⟩ |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
247 ( Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow f) ] ) (id1 A a) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
248 ≈⟨⟩ |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
249 hom b (id1 A a) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
250 ∎ |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
251 |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
252 |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
253 -- K{*}↓U has preinitial full subcategory then U is representable |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
254 -- K{*}↓U is complete, so it has initial object |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
255 |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
256 open SmallFullSubcategory |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
257 open PreInitial |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
258 |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
259 UisRepresentable : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
260 (U : Functor A (Sets {c₂}) ) |
617
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
261 (a : Obj (Sets {c₂})) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
262 (SFS : SmallFullSubcategory {c₁} {c₂} {ℓ} ( K (Sets {c₂}) A a ↓ U) ) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
263 (PI : PreInitial {c₁} {c₂} {ℓ} ( K (Sets) A a ↓ U) (SFSF SFS )) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
264 → Representable A U (obj (preinitialObj PI )) |
34540494fdcf
initital obj uniquness done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
616
diff
changeset
|
265 UisRepresentable A U a SFS PI = record { |
615
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
266 repr→ = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
267 ; repr← = record { TMap = {!!} ; isNTrans = record { commute = {!!} } } |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
268 ; reprId→ = λ {y} → ? |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
269 ; reprId← = λ {y} → ? |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
270 } |
a45c32ceca97
initial Object's arrow found
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
614
diff
changeset
|
271 |