Mercurial > hg > Members > kono > Proof > category
annotate SetsCompleteness.agda @ 532:d5d7163f2a1d
equalizer does not fit
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 29 Mar 2017 09:30:22 +0900 |
parents | 66cad3cb3a66 |
children | c3dcea3a92a7 |
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 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Category.Sets |
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 |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
105 open sequ |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
106 |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
107 -- equalizer-c = sequ a b f g |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
108 -- ; equalizer = λ e → equ e |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
109 |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
110 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
|
111 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
|
112 fe=ge = fe=ge |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
113 ; k = k |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
114 ; 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
|
115 ; uniqueness = uniqueness |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
116 } where |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
117 fe=ge0 : (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
118 fe=ge0 (elem x eq ) = eq |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
119 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
|
120 fe=ge = extensionality Sets (fe=ge0 ) |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
121 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 | 122 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
|
123 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
|
124 ek=h {d} {h} {eq} = refl |
520 | 125 irr : {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' |
126 irr refl refl = refl | |
523 | 127 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ |
128 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
|
129 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
|
130 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
|
131 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
|
132 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
|
133 lemma5 refl x = refl -- somehow this is not equal to lemma1 |
512 | 134 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)} → |
135 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] | |
525 | 136 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin |
137 k h fh=gh x | |
138 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ | |
139 k' x | |
140 ∎ ) where | |
141 open import Relation.Binary.PropositionalEquality | |
142 open ≡-Reasoning | |
143 | |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
144 |
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
145 open Functor |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
146 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
147 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
|
148 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
507 | 149 field |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
150 small→ : Obj C → I |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
151 small← : I → Obj C |
527 | 152 small-iso : { x : Obj C } → Hom C (small← ( small→ x )) x |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
153 shom→ : {i j : Obj C } → Hom C i j → I → I |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
154 shom← : {i j : I } → ( f : I → I ) → Hom C ( small← i ) ( small← j ) |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
155 shom-iso : {i j : I } → ( f : Hom C ( small← i ) ( small← j ) ) → C [ shom← ( shom→ f ) ≈ f ] |
507 | 156 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
157 open Small |
507 | 158 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
159 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : 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
|
160 (i : I ) → Set c₁ |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
161 ΓObj s Γ i = FObj Γ (small← s i ) |
507 | 162 |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
163 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : 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
|
164 {i j : I } → ( f : I → I ) → ΓObj s Γ i → ΓObj s Γ j |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
165 ΓMap s Γ {i} {j} f = FMap Γ ( shom← s f ) |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
166 |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
167 |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
168 record slim { c₂ } { I : Set c₂ } ( sobj : I → Set c₂ ) |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
169 ( smap : { i j : I } → (f : I → I )→ sobj i → sobj j ) : Set c₂ where |
527 | 170 field |
171 slim-obj : ( i : I ) → sobj i | |
530 | 172 slim-equ : {i j : I} ( f g : I → I ) → sequ I I f g |
507 | 173 |
527 | 174 open slim |
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
175 |
530 | 176 open import HomReasoning |
177 | |
178 open NTrans | |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
179 open IsEqualizer |
530 | 180 |
531 | 181 SetsNat : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
182 → NTrans C Sets (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ)) ) Γ | |
183 SetsNat C I s Γ = record { | |
184 TMap = λ i → Sets [ proj i o e ] | |
185 ; isNTrans = record { commute = comm1 } | |
530 | 186 } where |
531 | 187 e : Hom Sets (slim (ΓObj s Γ) (ΓMap s Γ)) (iproduct I (λ j → ΓObj s Γ j)) |
188 e = λ x → record { pi1 = λ j → slim-obj x j } | |
189 iid : {i : Obj C } → Hom Sets (FObj Γ (small← s (small→ s i))) (FObj Γ i) | |
190 iid {i} = FMap Γ ( small-iso s ) | |
191 proj : (i : Obj C ) → ( prod : iproduct I (λ j → ΓObj s Γ j )) → FObj Γ i | |
192 proj i prod = iid ( pi1 prod ( small→ s i ) ) | |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
193 equa : {b : Obj Sets } ( e : slim (ΓObj s Γ) (ΓMap s Γ) → iproduct I (λ j → ΓObj s Γ j) ) → ( f g : Hom Sets (iproduct I (λ j → ΓObj s Γ j)) b ) → |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
194 IsEqualizer Sets e f g |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
195 equa e f g = {!!} -- SetsIsEqualizer ? ? ? ? |
531 | 196 comm2 : {a b : Obj C} {f : Hom C a b} → ( x : slim (ΓObj s Γ) (ΓMap s Γ) ) → (Sets [ FMap Γ f o Sets [ proj a o e ] ]) x ≡ (Sets [ proj b o e ]) x |
197 comm2 {a} {b} {f} x = begin | |
198 (FMap Γ f ) ( ( proj a o e ) x ) | |
199 ≡⟨⟩ | |
200 (FMap Γ f ) ( iid ( slim-obj x (small→ s a) )) | |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
201 ≡⟨ {!!} ⟩ |
531 | 202 iid ( slim-obj x ( small→ s b ) ) |
203 ∎ where | |
204 open import Relation.Binary.PropositionalEquality | |
205 open ≡-Reasoning | |
206 comm1 : {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o Sets [ proj a o e ] ] ≈ | |
207 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] ] | |
208 comm1 {a} {b} {f} = begin | |
209 Sets [ FMap Γ f o Sets [ proj a o e ] ] | |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
210 ≈⟨ assoc ⟩ |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
211 Sets [ Sets [ FMap Γ f o proj a ] o e ] |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
212 ≈⟨ fe=ge (equa e ( Sets [ FMap Γ f o proj a ] ) (proj b )) ⟩ |
531 | 213 Sets [ proj b o e ] |
214 ≈↑⟨ idR ⟩ | |
215 Sets [ Sets [ proj b o e ] o id1 Sets (slim (ΓObj s Γ) (ΓMap s Γ)) ] | |
216 ≈⟨⟩ | |
217 Sets [ Sets [ proj b o e ] o FMap (K Sets C (slim (ΓObj s Γ) (ΓMap s Γ))) f ] | |
218 ∎ where | |
219 open ≈-Reasoning Sets | |
530 | 220 |
221 | |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
222 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
|
223 → Limit Sets C Γ |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
224 SetsLimit { c₂} C I s Γ = record { |
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
225 a0 = slim (ΓObj s Γ) (ΓMap s Γ) |
531 | 226 ; t0 = SetsNat C I s Γ |
523 | 227 ; isLimit = record { |
530 | 228 limit = limit1 |
523 | 229 ; t0f=t = {!!} |
230 ; limit-uniqueness = {!!} | |
231 } | |
232 } where | |
527 | 233 a0 : Obj Sets |
234 a0 = slim (ΓObj s Γ) (ΓMap s Γ) | |
235 e : Hom Sets a0 (iproduct I (λ j → ΓObj s Γ j)) | |
236 e = λ x → record { pi1 = λ j → slim-obj x j } | |
530 | 237 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (slim (ΓObj s Γ) (ΓMap s Γ)) |
238 limit1 = {!!} |