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