Mercurial > hg > Members > kono > Proof > category
annotate SetsCompleteness.agda @ 596:9367813d3f61
lemma-equ retry
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 23 May 2017 10:39:18 +0900 |
parents | 9676a75c3010 |
children | b281e8352158 |
rev | line source |
---|---|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Category -- https://github.com/konn/category-agda |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Level |
535 | 3 open import Category.Sets renaming ( _o_ to _*_ ) |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 module SetsCompleteness where |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import cat-utility |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Relation.Binary.Core |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Function |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
10 import Relation.Binary.PropositionalEquality |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
11 -- 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 ) |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
12 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
13 |
520 | 14 ≡cong = Relation.Binary.PropositionalEquality.cong |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
15 |
573 | 16 ≈-to-≡ : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → |
524 | 17 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x |
573 | 18 ≈-to-≡ refl x = refl |
503 | 19 |
504 | 20 record Σ {a} (A : Set a) (B : Set a) : Set a where |
503 | 21 constructor _,_ |
22 field | |
23 proj₁ : A | |
504 | 24 proj₂ : B |
503 | 25 |
26 open Σ public | |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} ) |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 SetsProduct { c₂ } = record { |
504 | 31 product = λ a b → Σ a b |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 ; π1 = λ a b → λ ab → (proj₁ ab) |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 ; π2 = λ a b → λ ab → (proj₂ ab) |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 ; isProduct = λ a b → record { |
503 | 35 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 ; π1fxg=f = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 ; π2fxg=g = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 ; uniqueness = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 } |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 } where |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b } |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ] |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 |
578 | 48 record sproduct {a} (I : Set a) ( Product : I → Set a ) : Set a where |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
49 field |
573 | 50 proj : ( i : I ) → Product i |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
51 |
578 | 52 open sproduct |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
53 |
578 | 54 iproduct1 : { c₂ : Level} → (I : Obj (Sets { c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (sproduct I fi) |
574 | 55 iproduct1 I fi {q} qi x = record { proj = λ i → (qi i) x } |
56 ipcx : { c₂ : Level} → (I : Obj (Sets { c₂})) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 I fi qi x ≡ iproduct1 I fi qi' x | |
57 ipcx I fi {q} {qi} {qi'} qi=qi x = | |
58 begin | |
59 record { proj = λ i → (qi i) x } | |
60 ≡⟨ ≡cong ( λ qi → record { proj = qi } ) ( extensionality Sets (λ i → ≈-to-≡ (qi=qi i) x )) ⟩ | |
61 record { proj = λ i → (qi' i) x } | |
62 ∎ where | |
63 open import Relation.Binary.PropositionalEquality | |
64 open ≡-Reasoning | |
65 ip-cong : { c₂ : Level} → (I : Obj (Sets { c₂}) ) (fi : I → Obj Sets ) {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 I fi qi ≈ iproduct1 I fi qi' ] | |
66 ip-cong I fi {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx I fi qi=qi ) | |
67 | |
570 | 68 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (fi : I → Obj Sets ) |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
69 → IProduct ( Sets { c₂} ) I |
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
70 SetsIProduct I fi = record { |
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
71 ai = fi |
578 | 72 ; iprod = sproduct I fi |
573 | 73 ; pi = λ i prod → proj prod i |
509 | 74 ; isIProduct = record { |
574 | 75 iproduct = iproduct1 I fi |
509 | 76 ; pif=q = pif=q |
77 ; ip-uniqueness = ip-uniqueness | |
574 | 78 ; ip-cong = ip-cong I fi |
509 | 79 } |
80 } where | |
574 | 81 pif=q : {q : Obj Sets} (qi : (i : I) → Hom Sets q (fi i)) {i : I} → Sets [ Sets [ (λ prod → proj prod i) o iproduct1 I fi qi ] ≈ qi i ] |
509 | 82 pif=q {q} qi {i} = refl |
578 | 83 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (sproduct I fi)} → Sets [ iproduct1 I fi (λ i → Sets [ (λ prod → proj prod i) o h ]) ≈ h ] |
509 | 84 ip-uniqueness = refl |
85 | |
86 | |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
87 -- |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
88 -- e f |
596 | 89 -- c -------→ a ---------→ b |
90 -- ^ . ---------→ | |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
91 -- | . g |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
92 -- |k . |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
93 -- | . h |
596 | 94 -- d |
509 | 95 |
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
96 -- cf. https://github.com/danr/Agda-projects/blob/master/Category-Theory/Equalizer.agda |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
97 |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
98 data sequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
99 elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
100 |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
101 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
102 equ (elem x eq) = x |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
103 |
533 | 104 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → |
105 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x | |
106 fe=ge0 (elem x eq ) = eq | |
107 | |
541 | 108 irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' |
109 irr refl refl = refl | |
110 | |
555 | 111 elm-cong : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y |
112 elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) | |
113 | |
563 | 114 fe=ge : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} |
115 → Sets [ Sets [ f o (λ e → equ {_} {a} {b} {f} {g} e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] | |
558 | 116 fe=ge = extensionality Sets (fe=ge0 ) |
117 k : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → {d : Obj Sets} (h : Hom Sets d a) | |
118 → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g) | |
573 | 119 k {_} {_} {_} {_} {_} {d} h eq = λ x → elem (h x) ( ≈-to-≡ eq x ) |
563 | 120 ek=h : { c₂ : Level} → {a b : Obj (Sets {c₂}) } {f g : Hom (Sets {c₂}) a b} → {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ {_} {a} {b} {f} {g} e ) o k h eq ] ≈ h ] |
558 | 121 ek=h {_} {_} {_} {_} {_} {d} {h} {eq} = refl |
122 | |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
123 open sequ |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
124 |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
125 -- equalizer-c = sequ a b f g |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
126 -- ; equalizer = λ e → equ e |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
127 |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
128 SetsIsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
129 SetsIsEqualizer {c₂} a b f g = record { |
560 | 130 fe=ge = fe=ge { c₂ } {a} {b} {f} {g} |
131 ; k = λ {d} h eq → k { c₂ } {a} {b} {f} {g} {d} h eq | |
558 | 132 ; ek=h = λ {d} {h} {eq} → ek=h {c₂} {a} {b} {f} {g} {d} {h} {eq} |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
133 ; uniqueness = uniqueness |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
134 } where |
523 | 135 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ |
136 injection f = ∀ x y → f x ≡ f y → x ≡ y | |
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
137 lemma5 : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → |
563 | 138 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ {_} {a} {b} {f} {g} (k h fh=gh x) ≡ equ (k' x) |
573 | 139 lemma5 refl x = refl -- somehow this is not equal to ≈-to-≡ |
512 | 140 uniqueness : {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} → |
141 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] | |
525 | 142 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin |
143 k h fh=gh x | |
144 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ | |
145 k' x | |
146 ∎ ) where | |
147 open import Relation.Binary.PropositionalEquality | |
148 open ≡-Reasoning | |
149 | |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
150 |
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
151 open Functor |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
152 |
538 | 153 ---- |
154 -- C is locally small i.e. Hom C i j is a set c₁ | |
155 -- | |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
156 record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
157 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
507 | 158 field |
552 | 159 hom→ : {i j : Obj C } → Hom C i j → I → I |
160 hom← : {i j : Obj C } → ( f : I → I ) → Hom C i j | |
540 | 161 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f |
536 | 162 -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y |
507 | 163 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
164 open Small |
507 | 165 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
166 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
538 | 167 (i : Obj C ) → Set c₁ |
168 ΓObj s Γ i = FObj Γ i | |
507 | 169 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
170 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
552 | 171 {i j : Obj C } → ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j |
540 | 172 ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
173 |
591 | 174 slid : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) → (x : Obj C) → I → I |
175 slid C I s x = hom→ s ( id1 C x ) | |
507 | 176 |
596 | 177 record slim { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) ( smap : { i j : OC } → (f : I → I ) → sobj i → sobj j ) |
558 | 178 : Set c₂ where |
179 field | |
596 | 180 slequ : { i j : OC } → ( f : I → I ) → sequ (sproduct OC sobj ) (sobj j) ( λ x → smap f ( proj x i ) ) ( λ x → proj x j ) |
181 slobj : OC → Set c₂ | |
182 slobj i = sobj i | |
183 slmap : {i j : OC } → (f : I → I ) → sobj i → sobj j | |
184 slmap f = smap f | |
185 ipp : {i j : OC } → (f : I → I ) → sproduct OC sobj | |
186 ipp {i} {j} f = equ ( slequ {i} {j} f ) | |
187 | |
591 | 188 open slim |
558 | 189 |
596 | 190 smap-id : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
191 ( se : slim (ΓObj s Γ) (ΓMap s Γ) ) → (i : Obj C ) → (x : FObj Γ i ) → slmap se (slid C I s i) x ≡ x | |
192 smap-id C I s Γ se i x = begin | |
193 slmap se (slid C I s i) x | |
194 ≡⟨⟩ | |
195 slmap se ( hom→ s (id1 C i)) x | |
196 ≡⟨⟩ | |
197 FMap Γ (hom← s (hom→ s (id1 C i))) x | |
198 ≡⟨ ≡cong ( λ ii → FMap Γ ii x ) (hom-iso s) ⟩ | |
199 FMap Γ (id1 C i) x | |
200 ≡⟨ ≡cong ( λ f → f x ) (IsFunctor.identity ( isFunctor Γ) ) ⟩ | |
201 x | |
202 ∎ where | |
590 | 203 open import Relation.Binary.PropositionalEquality |
204 open ≡-Reasoning | |
205 | |
586 | 206 |
596 | 207 product-to : { c₂ : Level } { I OC : Set c₂ } { sobj : OC → Set c₂ } |
208 → Hom Sets (sproduct OC sobj) (sproduct OC sobj) | |
209 product-to x = record { proj = proj x } | |
210 | |
211 lemma-equ' : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) | |
212 {i j : Obj C } → { f : I → I } | |
213 → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) | |
214 → proj (ipp se {i} {j} f) i ≡ proj (ipp se {i} {i} (slid C I s i) ) i | |
215 lemma-equ' C I s Γ {i} {j} {f} se = | |
216 fe=ge0 ? | |
590 | 217 |
596 | 218 lemma-equ : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
219 {i j i' j' : Obj C } → { f f' : I → I } | |
220 → (se : slim (ΓObj s Γ) (ΓMap s Γ) ) | |
221 → proj (ipp se {i} {j} f) i ≡ proj (ipp se {i'} {j'} f' ) i | |
222 lemma-equ C I s Γ {i} {j} {i'} {j'} {f} {f'} se = ≡cong ( λ p → proj p i ) ( begin | |
223 ipp se {i} {j} f | |
224 ≡⟨⟩ | |
225 record { proj = λ x → proj (equ (slequ se f)) x } | |
226 ≡⟨ ≡cong ( λ p → record { proj = proj p i }) ( ≡cong ( λ QIX → record { proj = QIX } ) ( | |
227 extensionality Sets ( λ x → ≡cong ( λ qi → qi x ) refl | |
228 ) )) ⟩ | |
229 record { proj = λ x → proj (equ (slequ se f')) x } | |
230 ≡⟨⟩ | |
231 ipp se {i'} {j'} f' | |
232 ∎ ) where | |
590 | 233 open import Relation.Binary.PropositionalEquality |
234 open ≡-Reasoning | |
235 | |
236 | |
596 | 237 open import HomReasoning |
238 open NTrans | |
590 | 239 |
589 | 240 |
553 | 241 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
596 | 242 → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) Γ |
243 Cone C I s Γ = record { | |
244 TMap = λ i → λ se → proj ( ipp se {i} {i} (λ x → x) ) i | |
564 | 245 ; isNTrans = record { commute = commute1 } |
530 | 246 } where |
596 | 247 commute1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → proj ( ipp se (λ x → x) ) a) ] ≈ |
248 Sets [ (λ se → proj ( ipp se (λ x → x) ) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ] ] | |
563 | 249 commute1 {a} {b} {f} = extensionality Sets ( λ se → begin |
596 | 250 (Sets [ FMap Γ f o (λ se₁ → proj ( ipp se (λ x → x) ) a) ]) se |
563 | 251 ≡⟨⟩ |
596 | 252 FMap Γ f (proj ( ipp se {a} {a} (λ x → x) ) a) |
253 ≡⟨ ≡cong ( λ g → FMap Γ g (proj ( ipp se {a} {a} (λ x → x) ) a)) (sym ( hom-iso s ) ) ⟩ | |
254 FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {a} (λ x → x) ) a) | |
255 ≡⟨ ≡cong ( λ g → FMap Γ (hom← s ( hom→ s f)) g ) ( lemma-equ C I s Γ se ) ⟩ | |
256 FMap Γ (hom← s ( hom→ s f)) (proj ( ipp se {a} {b} (hom→ s f) ) a) | |
257 ≡⟨ fe=ge0 ( slequ se (hom→ s f ) ) ⟩ | |
258 proj (ipp se {a} {b} ( hom→ s f )) b | |
259 ≡⟨ sym ( lemma-equ C I s Γ se ) ⟩ | |
260 proj (ipp se {b} {b} (λ x → x)) b | |
563 | 261 ≡⟨⟩ |
596 | 262 (Sets [ (λ se₁ → proj (ipp se₁ (λ x → x)) b) o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ) )) f ]) se |
562 | 263 ∎ ) where |
264 open import Relation.Binary.PropositionalEquality | |
265 open ≡-Reasoning | |
534 | 266 |
563 | 267 |
590 | 268 |
596 | 269 |
585 | 270 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
271 → Limit Sets C Γ | |
272 SetsLimit { c₂} C I s Γ = record { | |
596 | 273 a0 = slim (ΓObj s Γ) (ΓMap s Γ) |
587 | 274 ; t0 = Cone C I s Γ |
585 | 275 ; isLimit = record { |
596 | 276 limit = limit1 |
277 ; t0f=t = λ {a t i } → refl | |
278 ; limit-uniqueness = λ {a} {t} {f} → uniquness1 {a} {t} {f} | |
585 | 279 } |
280 } where | |
596 | 281 limit2 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } → ( f : I → I ) |
282 → ( x : a ) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x | |
283 limit2 a t f x = ≡cong ( λ g → g x ) ( IsNTrans.commute ( isNTrans t ) ) | |
284 limit1 : (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) ) | |
285 limit1 a t x = record { | |
286 slequ = λ {i} {j} f → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f x ) | |
287 } | |
288 uniquness2 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} | |
289 → ( i j : Obj C ) → | |
290 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → (f' : I → I ) → (x : a ) | |
291 → record { proj = λ i₁ → TMap t i₁ x } ≡ equ (slequ (f x) f') | |
292 uniquness2 {a} {t} {f} i j cif=t f' x = begin | |
293 record { proj = λ i → TMap t i x } | |
294 ≡⟨ ≡cong ( λ g → record { proj = λ i → g i } ) ( extensionality Sets ( λ i → sym ( ≡cong ( λ e → e x ) cif=t ) ) ) ⟩ | |
295 record { proj = λ i → (Sets [ TMap (Cone C I s Γ) i o f ]) x } | |
296 ≡⟨⟩ | |
297 record { proj = λ i → proj (ipp (f x) {i} {i} (λ x → x) ) i } | |
298 ≡⟨ ≡cong ( λ g → record { proj = λ i' → g i' } ) ( extensionality Sets ( λ i'' → lemma-equ C I s Γ (f x))) ⟩ | |
299 record { proj = λ i → proj (ipp (f x) f') i } | |
300 ∎ where | |
301 open import Relation.Binary.PropositionalEquality | |
302 open ≡-Reasoning | |
303 uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ) )} → | |
304 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] | |
305 uniquness1 {a} {t} {f} cif=t = extensionality Sets ( λ x → begin | |
306 limit1 a t x | |
307 ≡⟨⟩ | |
308 record { slequ = λ {i} {j} f' → elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x ) } | |
309 ≡⟨ ≡cong ( λ e → record { slequ = λ {i} {j} f' → e i j f' x } ) ( | |
310 extensionality Sets ( λ i → | |
311 extensionality Sets ( λ j → | |
312 extensionality Sets ( λ f' → | |
313 extensionality Sets ( λ x → | |
314 elm-cong ( elem ( record { proj = λ i → TMap t i x } ) ( limit2 a t f' x )) (slequ (f x) f' ) (uniquness2 {a} {t} {f} i j cif=t f' x ) ) | |
315 ))) | |
316 ) ⟩ | |
317 record { slequ = λ {i} {j} f' → slequ (f x ) f' } | |
318 ≡⟨⟩ | |
319 f x | |
320 ∎ ) where | |
321 open import Relation.Binary.PropositionalEquality | |
322 open ≡-Reasoning | |
323 |