Mercurial > hg > Members > kono > Proof > category
annotate src/SetsCompleteness.agda @ 1036:b836c3dc7a29
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 02 Apr 2021 11:26:44 +0900 |
| parents | 40c39d3e6a75 |
| children | 45de2b31bf02 |
| rev | line source |
|---|---|
| 606 | 1 open import Category -- https://github.com/konn/category-agda |
|
500
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 |
| 666 | 11 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → ( λ x → f x ≡ λ x → g x ) |
| 1034 | 12 -- import Axiom.Extensionality.Propositional |
| 13 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ | |
| 986 | 14 -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
15 |
| 606 | 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 |
| 781 | 18 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 19 | |
| 604 | 20 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → |
| 524 | 21 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x |
| 604 | 22 lemma1 refl x = refl |
| 503 | 23 |
| 504 | 24 record Σ {a} (A : Set a) (B : Set a) : Set a where |
| 503 | 25 constructor _,_ |
| 26 field | |
| 27 proj₁ : A | |
| 606 | 28 proj₂ : B |
| 503 | 29 |
| 30 open Σ public | |
|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 |
|
681
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
33 SetsProduct : { c₂ : Level} → ( a b : Obj (Sets {c₂})) → Product ( Sets { c₂} ) a b |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
34 SetsProduct { c₂ } a b = record { |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
35 product = Σ a b |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
36 ; π1 = λ ab → (proj₁ ab) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
37 ; π2 = λ ab → (proj₂ ab) |
|
bd8f7346f252
fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
676
diff
changeset
|
38 ; isProduct = record { |
| 606 | 39 _×_ = λ 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
|
40 ; π1fxg=f = refl |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 ; π2fxg=g = refl |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 ; uniqueness = refl |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 ; ×-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
|
44 } |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 } where |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 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
|
47 → 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
|
48 → 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
|
49 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
|
50 |
|
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
| 604 | 52 record iproduct {a} (I : Set a) ( pi0 : 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
|
53 field |
| 604 | 54 pi1 : ( i : I ) → pi0 i |
|
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
55 |
| 604 | 56 open iproduct |
| 574 | 57 |
| 986 | 58 open Small |
| 59 | |
| 606 | 60 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
61 → IProduct I ( Sets { c₂} ) ai |
|
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
62 SetsIProduct I fi = record { |
|
673
0007f9a25e9c
fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
672
diff
changeset
|
63 iprod = iproduct I fi |
| 604 | 64 ; pi = λ i prod → pi1 prod i |
| 509 | 65 ; isIProduct = record { |
| 604 | 66 iproduct = iproduct1 |
| 676 | 67 ; pif=q = λ {q} {qi} {i} → pif=q {q} {qi} {i} |
| 509 | 68 ; ip-uniqueness = ip-uniqueness |
| 604 | 69 ; ip-cong = ip-cong |
| 509 | 70 } |
| 71 } where | |
| 604 | 72 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi) |
| 73 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x } | |
| 676 | 74 pif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets q (fi i)} → {i : I} → Sets [ Sets [ (λ prod → pi1 prod i) o iproduct1 qi ] ≈ qi i ] |
| 75 pif=q {q} {qi} {i} = refl | |
| 604 | 76 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ] |
| 509 | 77 ip-uniqueness = refl |
| 604 | 78 ipcx : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → (x : q) → iproduct1 qi x ≡ iproduct1 qi' x |
| 606 | 79 ipcx {q} {qi} {qi'} qi=qi x = |
| 604 | 80 begin |
| 81 record { pi1 = λ i → (qi i) x } | |
| 82 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ | |
| 83 record { pi1 = λ i → (qi' i) x } | |
| 84 ∎ where | |
| 606 | 85 open import Relation.Binary.PropositionalEquality |
| 86 open ≡-Reasoning | |
| 604 | 87 ip-cong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets q (fi i)} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ iproduct1 qi ≈ iproduct1 qi' ] |
| 88 ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi ) | |
| 509 | 89 |
| 986 | 90 data coproduct {c} (a b : Set c) : Set c where |
| 91 k1 : ( i : a ) → coproduct a b | |
| 92 k2 : ( i : b ) → coproduct a b | |
| 93 | |
| 94 SetsCoProduct : { c₂ : Level} → (a b : Obj (Sets {c₂})) → coProduct Sets a b | |
| 95 SetsCoProduct a b = record { | |
| 96 coproduct = coproduct a b | |
| 97 ; κ1 = λ i → k1 i | |
| 98 ; κ2 = λ i → k2 i | |
| 99 ; isProduct = record { | |
| 100 _+_ = sum | |
| 101 ; κ1f+g=f = extensionality Sets (λ x → refl ) | |
| 102 ; κ2f+g=g = extensionality Sets (λ x → refl ) | |
| 103 ; uniqueness = λ {c} {h} → extensionality Sets (λ x → uniq {c} {h} x ) | |
| 104 ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → extensionality Sets (pccong feq geq) | |
| 105 } | |
| 106 } where | |
| 107 sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c | |
| 108 sum {c} f g (k1 i) = f i | |
| 109 sum {c} f g (k2 i) = g i | |
| 110 uniq : {c : Obj Sets} {h : Hom Sets (coproduct a b) c} → (x : coproduct a b ) → sum (Sets [ h o (λ i → k1 i) ]) (Sets [ h o (λ i → k2 i) ]) x ≡ h x | |
| 111 uniq {c} {h} (k1 i) = refl | |
| 112 uniq {c} {h} (k2 i) = refl | |
| 113 pccong : {c : Obj Sets} {f f' : Hom Sets a c} {g g' : Hom Sets b c} → f ≡ f' → g ≡ g' → (x : coproduct a b ) → sum f g x ≡ sum f' g' x | |
| 114 pccong refl refl (k1 i) = refl | |
| 115 pccong refl refl (k2 i) = refl | |
| 116 | |
| 117 | |
| 118 data icoproduct {a} (I : Set a) (ki : I → Set a) : Set a where | |
| 119 ki1 : (i : I) (x : ki i ) → icoproduct I ki | |
| 120 | |
| 121 SetsICoProduct : { c₂ : Level} → (I : Obj (Sets {c₂})) (ci : I → Obj Sets ) | |
| 122 → ICoProduct I ( Sets { c₂} ) ci | |
| 123 SetsICoProduct I fi = record { | |
| 124 icoprod = icoproduct I fi | |
| 125 ; ki = λ i x → ki1 i x | |
| 126 ; isICoProduct = record { | |
| 127 icoproduct = isum | |
| 128 ; kif=q = λ {q} {qi} {i} → kif=q {q} {qi} {i} | |
| 129 ; icp-uniqueness = uniq | |
| 130 ; icp-cong = iccong | |
| 131 } | |
| 132 } where | |
| 133 isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q | |
| 134 isum {q} fi (ki1 i x) = fi i x | |
| 135 kif=q : {q : Obj Sets} {qi : (i : I) → Hom Sets (fi i) q} {i : I} → Sets [ Sets [ isum qi o (λ x → ki1 i x) ] ≈ qi i ] | |
| 136 kif=q {q} {qi} {i} = extensionality Sets (λ x → refl ) | |
| 137 uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ] | |
| 138 uniq {q} {h} = extensionality Sets u1 where | |
| 139 u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x | |
| 140 u1 (ki1 i x) = refl | |
| 141 iccong : {q : Obj Sets} {qi qi' : (i : I) → Hom Sets (fi i) q} → ((i : I) → Sets [ qi i ≈ qi' i ]) → Sets [ isum qi ≈ isum qi' ] | |
| 142 iccong {q} {qi} {qi'} ieq = extensionality Sets u2 where | |
| 143 u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x | |
| 144 u2 (ki1 i x) = cong (λ k → k x ) (ieq i) | |
| 509 | 145 |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
146 -- |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
147 -- e f |
| 606 | 148 -- c -------→ a ---------→ b f ( f' |
| 604 | 149 -- ^ . ---------→ |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
150 -- | . g |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
151 -- |k . |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
152 -- | . h |
| 604 | 153 --y : d |
| 509 | 154 |
|
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
155 -- 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
|
156 |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
157 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
|
158 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
|
159 |
|
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
160 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a |
| 606 | 161 equ (elem x eq) = x |
|
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
162 |
| 606 | 163 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → |
| 533 | 164 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x |
| 165 fe=ge0 (elem x eq ) = eq | |
| 166 | |
| 541 | 167 irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' |
| 168 irr refl refl = refl | |
| 1032 | 169 elm-cong : { c₂ : Level} {a b : Set c₂} {f g : Hom (Sets {c₂}) a b} (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y |
| 170 elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) | |
| 541 | 171 |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
172 open sequ |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
173 |
|
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
174 -- equalizer-c = sequ a b f g |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
175 -- ; equalizer = λ e → equ e |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
176 |
| 669 | 177 SetsIsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g |
| 606 | 178 SetsIsEqualizer {c₂} a b f g = record { |
| 604 | 179 fe=ge = fe=ge |
| 180 ; k = k | |
| 181 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq} | |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
182 ; uniqueness = uniqueness |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
183 } where |
| 604 | 184 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] |
| 606 | 185 fe=ge = extensionality Sets (fe=ge0 ) |
| 604 | 186 k : {d : Obj Sets} (h : Hom Sets d a) → Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ] → Hom Sets d (sequ a b f g) |
| 187 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) | |
| 188 ek=h : {d : Obj Sets} {h : Hom Sets d a} {eq : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} → Sets [ Sets [ (λ e → equ e ) o k h eq ] ≈ h ] | |
| 606 | 189 ek=h {d} {h} {eq} = refl |
| 523 | 190 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ |
| 191 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
|
192 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)} → |
| 604 | 193 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) |
| 194 lemma5 refl x = refl -- somehow this is not equal to lemma1 | |
| 512 | 195 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)} → |
| 196 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] | |
| 525 | 197 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin |
| 198 k h fh=gh x | |
| 199 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ | |
| 200 k' x | |
| 201 ∎ ) where | |
| 202 open import Relation.Binary.PropositionalEquality | |
| 203 open ≡-Reasoning | |
| 204 | |
| 999 | 205 |
| 1009 | 206 -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c |
| 207 -- record cequ {c : Level} (A B : Set c) : Set (suc c) where | |
| 208 -- field | |
| 209 -- rev : {B : Set c} → (A → B) → B → A | |
| 210 -- surjective : {B : Set c } (x : B ) → (g : A → B) → g (rev g x) ≡ x | |
| 999 | 211 |
| 1009 | 212 -- -- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y |
| 213 -- -- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y | |
| 214 -- -- Y / R | |
| 215 | |
| 216 -- open import HomReasoning | |
| 986 | 217 |
| 1009 | 218 -- etsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) |
| 219 -- → IsCoEqualizer Sets (λ x → {!!} ) f g | |
| 220 -- etsIsCoEqualizer {c₂} a b f g = record { | |
| 221 -- ef=eg = extensionality Sets (λ x → {!!} ) | |
| 222 -- ; k = {!!} | |
| 223 -- ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} | |
| 224 -- ; uniqueness = {!!} | |
| 225 -- } where | |
| 226 -- c : Set c₂ | |
| 227 -- c = {!!} --cequ a b | |
| 228 -- d : cequ a b | |
| 229 -- d = {!!} | |
| 230 -- ef=eg : Sets [ Sets [ cequ.rev d f o f ] ≈ Sets [ cequ.rev d g o g ] ] | |
| 231 -- ef=eg = begin | |
| 232 -- Sets [ cequ.rev d f o f ] ≈↑⟨ idL ⟩ | |
| 233 -- Sets [ id1 Sets _ o Sets [ cequ.rev d f o f ] ] ≈↑⟨ assoc ⟩ | |
| 234 -- Sets [ Sets [ id1 Sets _ o cequ.rev d f ] o f ] ≈⟨ {!!} ⟩ | |
| 235 -- Sets [ Sets [ id1 Sets _ o cequ.rev d (id1 Sets _) ] o {!!} ] ≈⟨ car ( extensionality Sets (λ x → cequ.surjective d {!!} {!!} )) ⟩ | |
| 236 -- Sets [ {!!} o f ] ≈⟨ {!!} ⟩ | |
| 237 -- Sets [ id1 Sets _ o Sets [ cequ.rev d g o g ] ] ≈⟨ idL ⟩ | |
| 238 -- Sets [ cequ.rev d g o g ] ∎ where open ≈-Reasoning Sets | |
| 239 -- epi : { c₂ : Level } {a b c : Obj (Sets { c₂})} (e : Hom Sets b c ) → (f g : Hom Sets a b) → Set c₂ | |
| 240 -- epi e f g = Sets [ Sets [ e o f ] ≈ Sets [ e o g ] ] → Sets [ f ≈ g ] | |
| 241 -- k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d | |
| 242 -- k {d} h hf=hg = {!!} where | |
| 243 -- ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x)) | |
| 244 -- ca eq = {!!} | |
| 245 -- cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d | |
| 246 -- cd = {!!} | |
| 247 -- ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] } | |
| 248 -- → Sets [ Sets [ k h eq o {!!} ] ≈ h ] | |
| 249 -- ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin | |
| 250 -- k h eq ( {!!}) ≡⟨ {!!} ⟩ | |
| 251 -- h (f {!!}) ≡⟨ {!!} ⟩ | |
| 252 -- h (g {!!}) ≡⟨ {!!} ⟩ | |
| 253 -- h x | |
| 254 -- ∎ ) where | |
| 255 -- open import Relation.Binary.PropositionalEquality | |
| 256 -- open ≡-Reasoning | |
| 997 | 257 |
|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
258 |
|
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
259 open Functor |
|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
260 |
| 538 | 261 ---- |
| 262 -- C is locally small i.e. Hom C i j is a set c₁ | |
| 263 -- | |
| 986 | 264 -- record Small { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) |
| 265 -- : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where | |
| 266 -- field | |
| 267 -- hom→ : {i j : Obj C } → Hom C i j → I | |
| 268 -- hom← : {i j : Obj C } → ( f : I ) → Hom C i j | |
| 269 -- hom-iso : {i j : Obj C } → { f : Hom C i j } → C [ hom← ( hom→ f ) ≈ f ] | |
| 270 -- hom-rev : {i j : Obj C } → { f : I } → hom→ ( hom← {i} {j} f ) ≡ f | |
| 271 -- ≡←≈ : {i j : Obj C } → { f g : Hom C i j } → C [ f ≈ g ] → f ≡ g | |
| 507 | 272 |
| 606 | 273 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
| 538 | 274 (i : Obj C ) → Set c₁ |
| 275 ΓObj s Γ i = FObj Γ i | |
| 507 | 276 |
| 606 | 277 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
| 278 {i j : Obj C } → ( f : I ) → ΓObj s Γ i → ΓObj s Γ j | |
| 279 ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) | |
| 598 | 280 |
| 606 | 281 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) |
|
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
282 ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where |
| 606 | 283 field |
| 284 snmap : ( i : OC ) → sobj i | |
| 285 sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j | |
| 598 | 286 |
| 604 | 287 open snat |
|
600
3e2ef72d8d2f
Set Completeness unfinished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
599
diff
changeset
|
288 |
| 608 | 289 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' ) |
| 668 | 290 using (_≅_;refl; ≡-to-≅) |
| 669 | 291 -- why we cannot use Extensionality' ? |
| 292 postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → | |
| 293 {a : Level } {A : Set a} {B B' : A → Set a} | |
| 294 {f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y )) | |
| 608 | 295 |
|
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
296 snat-cong : {c : Level} |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
297 {I OC : Set c} |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
298 {sobj : OC → Set c} |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
299 {smap : {i j : OC} → (f : I) → sobj i → sobj j} |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
300 → (s t : snat sobj smap) |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
301 → (snmap-≡ : snmap s ≡ snmap t) |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
302 → (sncommute-≅ : sncommute s ≅ sncommute t) |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
303 → s ≡ t |
|
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
304 snat-cong _ _ refl refl = refl |
| 590 | 305 |
| 598 | 306 open import HomReasoning |
| 307 open NTrans | |
| 590 | 308 |
| 606 | 309 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
310 → NTrans C Sets (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ |
| 604 | 311 Cone C I s Γ = record { |
| 606 | 312 TMap = λ i → λ sn → snmap sn i |
| 604 | 313 ; isNTrans = record { commute = comm1 } |
| 598 | 314 } where |
| 604 | 315 comm1 : {a b : Obj C} {f : Hom C a b} → |
| 316 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
317 Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] |
| 604 | 318 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin |
| 319 FMap Γ f (snmap sn a ) | |
| 693 | 320 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩ |
| 604 | 321 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) |
| 596 | 322 ≡⟨⟩ |
| 606 | 323 ΓMap s Γ (hom→ s f) (snmap sn a ) |
| 324 ≡⟨ sncommute sn a b (hom→ s f) ⟩ | |
| 604 | 325 snmap sn b |
| 596 | 326 ∎ ) where |
| 590 | 327 open import Relation.Binary.PropositionalEquality |
| 328 open ≡-Reasoning | |
| 329 | |
| 330 | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
331 SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
|
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
332 → Limit C Sets Γ |
|
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
333 SetsLimit {c₁} I C s Γ = record { |
| 606 | 334 a0 = snat (ΓObj s Γ) (ΓMap s Γ) |
| 604 | 335 ; t0 = Cone C I s Γ |
| 598 | 336 ; isLimit = record { |
| 604 | 337 limit = limit1 |
| 338 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} | |
| 339 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} | |
| 598 | 340 } |
| 341 } where | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
342 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K C Sets a) Γ) (f : I) |
|
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
343 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x |
| 664 | 344 comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) ) |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
345 limit1 : (a : Obj Sets) → NTrans C Sets (K C Sets a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) |
| 604 | 346 limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; |
| 606 | 347 sncommute = λ i j f → comm2 t f } |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
348 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] |
| 604 | 349 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin |
| 350 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x | |
| 351 ≡⟨⟩ | |
| 352 TMap t i x | |
| 353 ∎ ) where | |
| 562 | 354 open import Relation.Binary.PropositionalEquality |
| 355 open ≡-Reasoning | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
356 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K C Sets a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → |
| 604 | 357 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] |
| 358 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin | |
| 598 | 359 limit1 a t x |
| 604 | 360 ≡⟨⟩ |
| 606 | 361 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } |
| 668 | 362 ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets ( λ i → eq1 x i )) (eq5 x ) ⟩ |
| 664 | 363 record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j g → sncommute (f x ) i j g } |
| 604 | 364 ≡⟨⟩ |
| 598 | 365 f x |
| 604 | 366 ∎ ) where |
| 598 | 367 open import Relation.Binary.PropositionalEquality |
| 368 open ≡-Reasoning | |
| 604 | 369 eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i |
| 370 eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t ) | |
| 669 | 371 eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x |
| 665 | 372 eq2 x i j f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) |
| 373 eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j | |
| 374 eq3 x i j k = sncommute (f x ) i j k | |
| 668 | 375 irr≅ : { c₂ : Level} {d e : Set c₂ } { x1 y1 : d } { x2 y2 : e } |
| 669 | 376 ( ee : x1 ≅ x2 ) ( ee' : y1 ≅ y2 ) ( eq : x1 ≡ y1 ) ( eq' : x2 ≡ y2 ) → eq ≅ eq' |
| 668 | 377 irr≅ refl refl refl refl = refl |
| 665 | 378 eq4 : ( x : a) ( i j : Obj C ) ( g : I ) |
| 379 → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ) ≅ sncommute (f x) i j g | |
| 668 | 380 eq4 x i j g = irr≅ (≡-to-≅ (≡cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g ) |
| 381 eq5 : ( x : a) | |
| 666 | 382 → ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } )) |
| 383 ≅ ( λ i j g → sncommute (f x) i j g ) | |
| 669 | 384 eq5 x = ≅extensionality (Sets {c₁} ) ( λ i → |
| 385 ≅extensionality (Sets {c₁} ) ( λ j → | |
| 386 ≅extensionality (Sets {c₁} ) ( λ g → eq4 x i j g ) ) ) | |
| 387 | |
| 388 open Limit | |
| 389 open IsLimit | |
| 672 | 390 open IProduct |
| 669 | 391 |
| 392 SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C | |
| 393 SetsCompleteness {c₁} {c₂} C I s = record { | |
|
691
917e51be9bbf
change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
681
diff
changeset
|
394 climit = λ Γ → SetsLimit {c₁} I C s Γ |
| 672 | 395 ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; |
| 396 equalizer = ( λ e → equ e ) ; | |
| 397 isEqualizer = SetsIsEqualizer a b f g } | |
| 398 ; cproduct = λ J fi → SetsIProduct J fi | |
| 669 | 399 } where |