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