Mercurial > hg > Members > kono > Proof > category
annotate SetsCompleteness.agda @ 550:c2ce1c6a3570
close this
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Apr 2017 03:24:44 +0900 |
| parents | adef39d19884 |
| children |
| 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 |
| 524 | 18 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → |
| 19 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x | |
| 20 lemma1 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 |
|
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
50 record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
51 field |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
52 pi1 : ( i : I ) → pi0 i |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
53 |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
54 open iproduct |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
55 |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
56 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
57 → IProduct ( Sets { c₂} ) I |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
58 SetsIProduct I fi = record { |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
59 ai = fi |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
60 ; iprod = iproduct I fi |
|
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
61 ; pi = λ i prod → pi1 prod i |
| 509 | 62 ; isIProduct = record { |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
63 iproduct = iproduct1 |
| 509 | 64 ; pif=q = pif=q |
| 65 ; ip-uniqueness = ip-uniqueness | |
| 66 ; ip-cong = ip-cong | |
| 67 } | |
| 68 } where | |
| 69 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi) | |
| 70 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x } | |
| 71 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 ] | |
| 72 pif=q {q} qi {i} = refl | |
| 73 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ] | |
| 74 ip-uniqueness = refl | |
| 75 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 | |
| 76 ipcx {q} {qi} {qi'} qi=qi x = | |
| 77 begin | |
| 78 record { pi1 = λ i → (qi i) x } | |
| 520 | 79 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ |
| 509 | 80 record { pi1 = λ i → (qi' i) x } |
| 81 ∎ where | |
| 82 open import Relation.Binary.PropositionalEquality | |
| 83 open ≡-Reasoning | |
| 84 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' ] | |
| 85 ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi ) | |
| 86 | |
| 87 | |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
88 -- |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
89 -- e f |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
90 -- c -------→ a ---------→ b f ( f' |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
91 -- ^ . ---------→ |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
92 -- | . g |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
93 -- |k . |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
94 -- | . h |
| 514 | 95 --y : d |
| 509 | 96 |
|
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
97 -- 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
|
98 |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
99 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
|
100 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
|
101 |
|
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
102 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
|
103 equ (elem x eq) = x |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
104 |
| 533 | 105 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → |
| 106 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x | |
| 107 fe=ge0 (elem x eq ) = eq | |
| 108 | |
| 541 | 109 irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' |
| 110 irr refl refl = refl | |
| 111 | |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
112 open sequ |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
113 |
|
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
114 -- equalizer-c = sequ a b f g |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
115 -- ; equalizer = λ e → equ e |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
116 |
|
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
117 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
|
118 SetsIsEqualizer {c₂} a b f g = record { |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
119 fe=ge = fe=ge |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
120 ; k = k |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
121 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq} |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
122 ; uniqueness = uniqueness |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
123 } where |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
124 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
125 fe=ge = extensionality Sets (fe=ge0 ) |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
126 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) |
| 520 | 127 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) |
|
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
128 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 ] |
|
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
129 ek=h {d} {h} {eq} = refl |
| 523 | 130 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ |
| 131 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
|
132 elm-cong : (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y |
|
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
133 elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) |
|
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
134 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)} → |
|
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
135 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) |
|
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
136 lemma5 refl x = refl -- somehow this is not equal to lemma1 |
| 512 | 137 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)} → |
| 138 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] | |
| 525 | 139 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin |
| 140 k h fh=gh x | |
| 141 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ | |
| 142 k' x | |
| 143 ∎ ) where | |
| 144 open import Relation.Binary.PropositionalEquality | |
| 145 open ≡-Reasoning | |
| 146 | |
|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 |
|
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
148 open Functor |
|
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
149 |
| 538 | 150 ---- |
| 151 -- C is locally small i.e. Hom C i j is a set c₁ | |
| 152 -- | |
|
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
153 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
|
154 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
| 507 | 155 field |
| 540 | 156 hom→ : {i j : Obj C } → Hom C i j → I |
| 157 hom← : {i j : Obj C } → ( f : I ) → Hom C i j | |
| 158 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f | |
| 536 | 159 -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } → (x≈y : C [ x ≈ y ] ) → x ≡ y |
| 507 | 160 |
|
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
161 open Small |
| 507 | 162 |
|
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
163 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
| 538 | 164 (i : Obj C ) → Set c₁ |
| 165 ΓObj s Γ i = FObj Γ i | |
| 507 | 166 |
|
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
167 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
| 539 | 168 {i j : Obj C } → ( f : I ) → ΓObj s Γ i → ΓObj s Γ j |
| 540 | 169 Γ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
|
170 |
| 538 | 171 record snat { c₂ } { I OC : Set c₂ } ( sobj : OC → Set c₂ ) |
| 539 | 172 ( smap : { i j : OC } → (f : I )→ sobj i → sobj j ) : Set c₂ where |
| 527 | 173 field |
| 538 | 174 snmap : ( i : OC ) → sobj i |
| 539 | 175 sncommute : { i j : OC } → ( f : I ) → smap f ( snmap i ) ≡ snmap j |
| 507 | 176 |
| 534 | 177 open snat |
|
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
178 |
| 548 | 179 snmeq : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j } |
| 180 ( s t : snat SO SM ) → ( i : OC ) → | |
| 181 { snmapsi snmapti : SO i } → snmapsi ≡ snmapti → SO i | |
| 182 snmeq s t i {pi} {.pi} refl = pi | |
| 183 | |
| 184 snmc : { c₂ : Level } { I OC : Set c₂ } { SO : OC → Set c₂ } { SM : { i j : OC } → (f : I )→ SO i → SO j } | |
| 185 ( s t : snat SO SM ) → { i j : OC } → { f : I } → | |
| 186 { snmapsi snmapti : SO i } → (eqi : snmapsi ≡ snmapti ) → | |
| 187 { snmapsj snmaptj : SO j } → (eqj : snmapsj ≡ snmaptj ) | |
| 188 → ( SM f ( snmapsi ) ≡ snmapsj ) | |
| 189 → ( SM f ( snmapti ) ≡ snmaptj ) | |
| 190 → SM f (snmeq s t i (eqi)) ≡ snmeq s t j (eqj) | |
| 191 snmc s t refl refl refl refl = refl | |
| 192 | |
| 193 snat1 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) | |
| 194 → ( s t : snat SO SM ) | |
| 195 → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) | |
| 196 → ( eq2 : ( i j : OC ) ( f : I ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j ) | |
| 197 → ( eq3 : ( i j : OC ) ( f : I ) → SM {i} {j} f ( snmap t i ) ≡ snmap t j ) | |
| 198 → snat SO SM | |
| 199 snat1 SO SM s t eq1 eq2 eq3 = record { | |
| 200 snmap = λ i → snmeq s t i (eq1 i ) ; | |
| 201 sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f ) | |
| 202 } | |
| 546 | 203 |
| 549 | 204 ≡cong2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → B → C ) |
| 541 | 205 → a ≡ a' |
| 206 → b ≡ b' | |
| 207 → f a b ≡ f a' b' | |
| 208 ≡cong2 _ refl refl = refl | |
| 209 | |
| 549 | 210 subst2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → C ) ( g : B → C ) |
| 211 → f a ≡ g b | |
| 212 → a ≡ a' | |
| 213 → b ≡ b' | |
| 214 → f a' ≡ g b' | |
| 215 subst2 {_} {_} {A} {B} {C} { a} {.a} {b} {.b} f g f=g refl refl = f=g | |
| 216 | |
| 548 | 217 snmeqeqs : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) |
| 218 ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) → | |
| 549 | 219 snmap s i ≡ snmeq s t i (eq1 i ) |
| 548 | 220 snmeqeqs SO SM s t i eq1 = lemma (eq1 i) refl where |
| 221 lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapsi ≡ sm ) → | |
| 549 | 222 sm ≡ snmeq s t i eq1 |
| 548 | 223 lemma refl refl = refl |
| 224 | |
| 225 snmeqeqt : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) | |
| 226 ( s t : snat SO SM ) → ( i : OC ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) → | |
| 549 | 227 snmap t i ≡ snmeq s t i (eq1 i ) |
| 548 | 228 snmeqeqt SO SM s t i eq1 = lemma (eq1 i) refl where |
| 229 lemma : { snmapsi snmapti sm : SO i } → ( eq1 : snmapsi ≡ snmapti ) → ( snmapti ≡ sm ) → | |
| 549 | 230 sm ≡ snmeq s t i eq1 |
| 548 | 231 lemma refl refl = refl |
| 232 | |
| 549 | 233 scomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) |
| 234 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) | |
| 235 → ( i j : OC ) → ( f : I ) | |
| 236 → SM f ( snmap s i ) ≡ snmap s j | |
| 550 | 237 → {x : ( i : OC ) → SO i } → (x ≡ λ i → snmeq s t i (eq1 i ) ) |
| 238 → SM f (x i) ≡ x j | |
| 239 scomm2 SO SM s t eq1 i j f eq2 refl = lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1) where | |
| 549 | 240 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) |
| 241 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 | |
| 242 | |
| 243 tcomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) | |
| 244 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) | |
| 245 → ( i j : OC ) → ( f : I ) | |
| 246 → SM f ( snmap t i ) ≡ snmap t j | |
| 247 → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j) | |
| 248 tcomm2 SO SM s t eq1 i j f eq2 = lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt SO SM s t j eq1) where | |
| 249 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) | |
| 250 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 | |
| 251 | |
| 252 | |
| 543 | 253 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j) |
| 254 { s t : snat SObj SMap } | |
| 255 → (( i : OC ) → snmap s i ≡ snmap t i ) | |
| 256 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) | |
| 257 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) | |
| 258 → s ≡ t | |
| 550 | 259 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = begin |
| 260 record { snmap = λ i → snmap s i ; sncommute = λ {i} {j} f → sncommute s f } | |
| 261 ≡⟨ | |
| 262 ≡cong2 ( λ x y → | |
| 263 record { snmap = λ i → x i ; sncommute = λ {i} {j} f → y ? i j f } ) ( extensionality Sets ( λ i → snmeqeqs SO SM s t i eq1 ) ) | |
| 264 ( extensionality Sets ( λ x → | |
| 265 ( extensionality Sets ( λ i → | |
| 266 ( extensionality Sets ( λ j → | |
| 267 ( extensionality Sets ( λ f → scomm2 SO SM s t eq1 i j f (eq2 i j f ) x | |
| 268 )))))))) | |
| 269 ⟩ | |
| 270 record { snmap = λ i → snmeq s t i (eq1 i ) ; sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f ) } | |
| 271 ≡⟨ {!!} ⟩ | |
| 272 record { snmap = λ i → snmap t i ; sncommute = λ {i} {j} f → sncommute t f } | |
| 273 ∎ where | |
| 274 open import Relation.Binary.PropositionalEquality | |
| 275 open ≡-Reasoning | |
| 543 | 276 |
| 530 | 277 open import HomReasoning |
| 278 open NTrans | |
| 533 | 279 |
| 535 | 280 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
| 534 | 281 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ |
| 535 | 282 Cone C I s Γ = record { |
| 538 | 283 TMap = λ i → λ sn → snmap sn i |
| 531 | 284 ; isNTrans = record { commute = comm1 } |
| 530 | 285 } where |
| 534 | 286 comm1 : {a b : Obj C} {f : Hom C a b} → |
| 538 | 287 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ |
| 288 Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] | |
| 534 | 289 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin |
| 538 | 290 FMap Γ f (snmap sn a ) |
| 540 | 291 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ |
| 292 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) | |
| 535 | 293 ≡⟨⟩ |
| 540 | 294 ΓMap s Γ (hom→ s f) (snmap sn a ) |
| 295 ≡⟨ sncommute sn (hom→ s f) ⟩ | |
| 538 | 296 snmap sn b |
| 534 | 297 ∎ ) where |
| 298 open import Relation.Binary.PropositionalEquality | |
| 299 open ≡-Reasoning | |
| 300 | |
| 530 | 301 |
|
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
302 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
|
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
303 → Limit Sets C Γ |
|
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
304 SetsLimit { c₂} C I s Γ = record { |
| 534 | 305 a0 = snat (ΓObj s Γ) (ΓMap s Γ) |
| 535 | 306 ; t0 = Cone C I s Γ |
| 523 | 307 ; isLimit = record { |
| 530 | 308 limit = limit1 |
| 539 | 309 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} |
| 310 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} | |
| 311 } | |
| 523 | 312 } where |
| 527 | 313 a0 : Obj Sets |
| 534 | 314 a0 = snat (ΓObj s Γ) (ΓMap s Γ) |
| 539 | 315 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) |
| 538 | 316 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x |
| 317 comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) | |
| 534 | 318 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) |
| 538 | 319 limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; |
| 537 | 320 sncommute = λ f → comm2 t f } |
| 539 | 321 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o limit1 a t ] ≈ TMap t i ] |
| 540 | 322 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin |
| 323 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x | |
| 324 -- ≡⟨⟩ | |
| 325 -- snmap ( record { snmap = λ i → ( TMap t i ) x ; sncommute = λ {i j} f → comm2 {a} {x} {i} {j} t f } ) i | |
| 326 ≡⟨⟩ | |
| 327 TMap t i x | |
| 328 ∎ ) where | |
| 329 open import Relation.Binary.PropositionalEquality | |
| 330 open ≡-Reasoning | |
| 539 | 331 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → |
| 332 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] | |
| 540 | 333 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin |
| 334 limit1 a t x | |
| 335 ≡⟨⟩ | |
| 336 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ f → comm2 t f } | |
| 548 | 337 ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) (eq1 x) (eq2 x ) (eq3 x ) ⟩ |
| 541 | 338 record { snmap = λ i → snmap (f x ) i ; sncommute = sncommute (f x ) } |
| 540 | 339 ≡⟨⟩ |
| 340 f x | |
| 341 ∎ ) where | |
| 342 open import Relation.Binary.PropositionalEquality | |
| 343 open ≡-Reasoning | |
| 548 | 344 eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i |
| 345 eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t ) | |
| 346 eq2 : (x : a ) (i j : Obj C) (f : I) → ΓMap s Γ f (TMap t i x) ≡ TMap t j x | |
| 347 eq2 x i j f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) | |
| 348 eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j | |
| 349 eq3 x i j k = sncommute (f x ) k | |
| 537 | 350 |
| 351 | |
| 352 | |
| 353 | |
| 354 | |
| 355 | |
| 356 | |
| 539 | 357 |
| 358 | |
| 548 | 359 |