Mercurial > hg > Members > kono > Proof > category
annotate SetsCompleteness.agda @ 665:9904edf40547
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 23 Oct 2017 07:52:30 +0900 |
parents | 9e8276b89cd0 |
children | ba84fbc64c7d |
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 |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
11 -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
12 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
13 |
606 | 14 ≡cong = Relation.Binary.PropositionalEquality.cong |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
15 |
604 | 16 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → |
524 | 17 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x |
604 | 18 lemma1 refl x = refl |
503 | 19 |
504 | 20 record Σ {a} (A : Set a) (B : Set a) : Set a where |
503 | 21 constructor _,_ |
22 field | |
23 proj₁ : A | |
606 | 24 proj₂ : B |
503 | 25 |
26 open Σ public | |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} ) |
606 | 30 SetsProduct { c₂ } = record { |
504 | 31 product = λ a b → Σ a b |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 ; π1 = λ a b → λ ab → (proj₁ ab) |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 ; π2 = λ a b → λ ab → (proj₂ ab) |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 ; isProduct = λ a b → record { |
606 | 35 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 ; π1fxg=f = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 ; π2fxg=g = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 ; uniqueness = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 } |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 } where |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b } |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ] |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 |
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 |
604 | 48 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
|
49 field |
604 | 50 pi1 : ( i : I ) → pi0 i |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
51 |
604 | 52 open iproduct |
574 | 53 |
606 | 54 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets ) |
508
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
55 → IProduct ( Sets { c₂} ) I |
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
56 SetsIProduct I fi = record { |
3ce21b2a671a
IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
507
diff
changeset
|
57 ai = fi |
604 | 58 ; iprod = iproduct I fi |
59 ; pi = λ i prod → pi1 prod i | |
509 | 60 ; isIProduct = record { |
604 | 61 iproduct = iproduct1 |
509 | 62 ; pif=q = pif=q |
63 ; ip-uniqueness = ip-uniqueness | |
604 | 64 ; ip-cong = ip-cong |
509 | 65 } |
66 } where | |
604 | 67 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi) |
68 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x } | |
69 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 ] | |
509 | 70 pif=q {q} qi {i} = refl |
604 | 71 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ] |
509 | 72 ip-uniqueness = refl |
604 | 73 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 | 74 ipcx {q} {qi} {qi'} qi=qi x = |
604 | 75 begin |
76 record { pi1 = λ i → (qi i) x } | |
77 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ | |
78 record { pi1 = λ i → (qi' i) x } | |
79 ∎ where | |
606 | 80 open import Relation.Binary.PropositionalEquality |
81 open ≡-Reasoning | |
604 | 82 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' ] |
83 ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi ) | |
509 | 84 |
85 | |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
86 -- |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
87 -- e f |
606 | 88 -- c -------→ a ---------→ b f ( f' |
604 | 89 -- ^ . ---------→ |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
90 -- | . g |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
91 -- |k . |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
92 -- | . h |
604 | 93 --y : d |
509 | 94 |
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
95 -- 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
|
96 |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
97 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
|
98 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
|
99 |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
100 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a |
606 | 101 equ (elem x eq) = x |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
102 |
606 | 103 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → |
533 | 104 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x |
105 fe=ge0 (elem x eq ) = eq | |
106 | |
541 | 107 irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq' |
108 irr refl refl = refl | |
109 | |
510
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
110 open sequ |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
111 |
532
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
112 -- equalizer-c = sequ a b f g |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
113 -- ; equalizer = λ e → equ e |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
114 |
d5d7163f2a1d
equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
531
diff
changeset
|
115 SetsIsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g |
606 | 116 SetsIsEqualizer {c₂} a b f g = record { |
604 | 117 fe=ge = fe=ge |
118 ; k = k | |
119 ; 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
|
120 ; uniqueness = uniqueness |
5eb4b69bf541
equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
509
diff
changeset
|
121 } where |
604 | 122 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] |
606 | 123 fe=ge = extensionality Sets (fe=ge0 ) |
604 | 124 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) |
125 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) | |
126 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 | 127 ek=h {d} {h} {eq} = refl |
523 | 128 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ |
129 injection f = ∀ x y → f x ≡ f y → x ≡ y | |
604 | 130 elm-cong : (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y |
131 elm-cong ( elem x eq ) (elem .x eq' ) refl = ≡cong ( λ ee → elem x ee ) ( irr eq eq' ) | |
522
8fd030f9f572
Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
521
diff
changeset
|
132 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 | 133 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) |
134 lemma5 refl x = refl -- somehow this is not equal to lemma1 | |
512 | 135 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)} → |
136 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] | |
525 | 137 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin |
138 k h fh=gh x | |
139 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ | |
140 k' x | |
141 ∎ ) where | |
142 open import Relation.Binary.PropositionalEquality | |
143 open ≡-Reasoning | |
144 | |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
145 |
501
61daa68a70c4
Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
500
diff
changeset
|
146 open Functor |
500
6c993c1fe9de
try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
147 |
538 | 148 ---- |
149 -- C is locally small i.e. Hom C i j is a set c₁ | |
150 -- | |
526
b035cd3be525
Small Category for Sets Limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
525
diff
changeset
|
151 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
|
152 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where |
507 | 153 field |
606 | 154 hom→ : {i j : Obj C } → Hom C i j → I |
155 hom← : {i j : Obj C } → ( f : I ) → Hom C i j | |
156 hom-iso : {i j : Obj C } → { f : Hom C i j } → hom← ( hom→ f ) ≡ f | |
507 | 157 |
606 | 158 open Small |
507 | 159 |
606 | 160 ΓObj : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
538 | 161 (i : Obj C ) → Set c₁ |
162 ΓObj s Γ i = FObj Γ i | |
507 | 163 |
606 | 164 ΓMap : { c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I : Set c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} )) |
165 {i j : Obj C } → ( f : I ) → ΓObj s Γ i → ΓObj s Γ j | |
166 ΓMap s Γ {i} {j} f = FMap Γ ( hom← s f ) | |
598 | 167 |
606 | 168 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
|
169 ( smap : { i j : OC } → (f : I ) → sobj i → sobj j ) : Set c₂ where |
606 | 170 field |
171 snmap : ( i : OC ) → sobj i | |
172 sncommute : ( i j : OC ) → ( f : I ) → smap f ( snmap i ) ≡ snmap j | |
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
173 smap0 : { i j : OC } → (f : I ) → sobj i → sobj j |
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
174 smap0 {i} {j} f x = smap f x |
598 | 175 |
604 | 176 open snat |
600
3e2ef72d8d2f
Set Completeness unfinished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
599
diff
changeset
|
177 |
608 | 178 ≡cong2 : { c c' : Level } { A B : Set c } { C : Set c' } { a a' : A } { b b' : B } ( f : A → B → C ) |
179 → a ≡ a' | |
180 → b ≡ b' | |
181 → f a b ≡ f a' b' | |
182 ≡cong2 _ refl refl = refl | |
183 | |
184 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' ) | |
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
185 using (_≅_;refl) |
664 | 186 postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂ |
608 | 187 |
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
188 snat-cong : {c : Level} |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
189 {I OC : Set c} |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
190 {sobj : OC → Set c} |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
191 {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
|
192 → (s t : snat sobj smap) |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
193 → (snmap-≡ : snmap s ≡ snmap t) |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
194 → (sncommute-≅ : sncommute s ≅ sncommute t) |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
195 → s ≡ t |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
196 snat-cong _ _ refl refl = refl |
590 | 197 |
598 | 198 open import HomReasoning |
199 open NTrans | |
590 | 200 |
606 | 201 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
604 | 202 → NTrans C Sets (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ) ) ) Γ |
203 Cone C I s Γ = record { | |
606 | 204 TMap = λ i → λ sn → snmap sn i |
604 | 205 ; isNTrans = record { commute = comm1 } |
598 | 206 } where |
604 | 207 comm1 : {a b : Obj C} {f : Hom C a b} → |
208 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ | |
209 Sets [ (λ sn → (snmap sn b)) o FMap (K Sets C (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] | |
210 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin | |
211 FMap Γ f (snmap sn a ) | |
212 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( hom-iso s )) ⟩ | |
213 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) | |
596 | 214 ≡⟨⟩ |
606 | 215 ΓMap s Γ (hom→ s f) (snmap sn a ) |
216 ≡⟨ sncommute sn a b (hom→ s f) ⟩ | |
604 | 217 snmap sn b |
596 | 218 ∎ ) where |
590 | 219 open import Relation.Binary.PropositionalEquality |
220 open ≡-Reasoning | |
221 | |
222 | |
606 | 223 SetsLimit : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) |
598 | 224 → Limit Sets C Γ |
606 | 225 SetsLimit { c₂} C I s Γ = record { |
226 a0 = snat (ΓObj s Γ) (ΓMap s Γ) | |
604 | 227 ; t0 = Cone C I s Γ |
598 | 228 ; isLimit = record { |
604 | 229 limit = limit1 |
230 ; t0f=t = λ {a t i } → t0f=t {a} {t} {i} | |
231 ; limit-uniqueness = λ {a t i } → limit-uniqueness {a} {t} {i} | |
598 | 232 } |
233 } where | |
606 | 234 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) |
605
af321e38ecee
another snat-cong approach
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
604
diff
changeset
|
235 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x |
664 | 236 comm2 {a} {x} t f = ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) ) |
606 | 237 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) |
604 | 238 limit1 a t = λ x → record { snmap = λ i → ( TMap t i ) x ; |
606 | 239 sncommute = λ i j f → comm2 t f } |
604 | 240 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 ] |
241 t0f=t {a} {t} {i} = extensionality Sets ( λ x → begin | |
242 ( Sets [ TMap (Cone C I s Γ) i o limit1 a t ]) x | |
243 ≡⟨⟩ | |
244 TMap t i x | |
245 ∎ ) where | |
562 | 246 open import Relation.Binary.PropositionalEquality |
247 open ≡-Reasoning | |
604 | 248 limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ))} → |
249 ({i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t ≈ f ] | |
250 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin | |
598 | 251 limit1 a t x |
604 | 252 ≡⟨⟩ |
606 | 253 record { snmap = λ i → ( TMap t i ) x ; sncommute = λ i j f → comm2 t f } |
665 | 254 ≡⟨ snat-cong (limit1 a t x) (f x ) ( extensionality Sets ( λ i → eq1 x i )) (eq5 x ) ⟩ |
664 | 255 record { snmap = λ i → snmap (f x ) i ; sncommute = λ i j g → sncommute (f x ) i j g } |
604 | 256 ≡⟨⟩ |
598 | 257 f x |
604 | 258 ∎ ) where |
598 | 259 open import Relation.Binary.PropositionalEquality |
260 open ≡-Reasoning | |
604 | 261 eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i |
262 eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t ) | |
665 | 263 eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x -- hg cat -r 550 SetsCompleteness.agda |
264 eq2 x i j f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) | |
265 eq3 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j | |
266 eq3 x i j k = sncommute (f x ) i j k | |
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
267 irr≅ : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≅ eq' |
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
268 irr≅ refl refl = refl |
665 | 269 eq4 : ( x : a) ( i j : Obj C ) ( g : I ) |
270 → TMap t i x ≡ snmap (f x) i | |
271 → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ) ≅ sncommute (f x) i j g | |
272 eq4 x i j g eq = {!!} -- irr≅ ? ? | |
663
855e497a9c8f
introducd HeterogeneousEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
608
diff
changeset
|
273 -- eq2 : ( x : a) → sncommute (limit1 a t x) ≅ sncommute (f x) |
665 | 274 eq5 : ( x : a) → ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } )) |
664 | 275 ≅ ( λ i j g → sncommute (f x) i j g ) |
665 | 276 eq5 x = {!!} |