Mercurial > hg > Members > kono > Proof > category

comparison src/SetsCompleteness.agda @ 1112:0e750446e463

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Nov 2023 08:49:21 +0900
parents 45de2b31bf02
children
comparison
equal deleted inserted replaced
1111:73c72679421c 1112:0e750446e463
1 {-# OPTIONS --cubical-compatible --safe #-} 1 {-# OPTIONS #-}
2 2
3 open import Category -- https://github.com/konn/category-agda 3 open import Category -- https://github.com/konn/category-agda
4 open import Level 4 open import Level
5 open import Category.Sets renaming ( _o_ to _*_ ) 5 open import Category.Sets renaming ( _o_ to _*_ )
6 6
9 open import Definitions 9 open import Definitions
10 open import Relation.Binary.Core 10 open import Relation.Binary.Core
11 open import Function 11 open import Function
12 import Relation.Binary.PropositionalEquality 12 import Relation.Binary.PropositionalEquality
13 -- 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 ) 13 -- 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 )
14 -- import Axiom.Extensionality.Propositional 14
15 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂ 15 import Axiom.Extensionality.Propositional
16 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality c₂ c₂
17
16 -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂ 18 -- Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
17 19
18 ≡cong = Relation.Binary.PropositionalEquality.cong 20 ≡cong = Relation.Binary.PropositionalEquality.cong
19 21
20 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 22 open import Relation.Binary.PropositionalEquality hiding ( [_] )
21 23
22 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} → 24 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} →
23 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x 25 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x
24 lemma1 refl x = refl 26 lemma1 eq x = ?
25 27
26 record Σ {a} (A : Set a) (B : Set a) : Set a where 28 record Σ {a} (A : Set a) (B : Set a) : Set a where
27 constructor _,_ 29 constructor _,_
28 field 30 field
29 proj₁ : A 31 proj₁ : A
37 product = Σ a b 39 product = Σ a b
38 ; π1 = λ ab → (proj₁ ab) 40 ; π1 = λ ab → (proj₁ ab)
39 ; π2 = λ ab → (proj₂ ab) 41 ; π2 = λ ab → (proj₂ ab)
40 ; isProduct = record { 42 ; isProduct = record {
41 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) 43 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x )
42 ; π1fxg=f = refl 44 ; π1fxg=f = ?
43 ; π2fxg=g = refl 45 ; π2fxg=g = ?
44 ; uniqueness = refl 46 ; uniqueness = ?
45 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g 47 ; ×-cong = λ {c} {f} {f'} {g} {g'} f=f g=g → prod-cong a b f=f g=g
46 } 48 }
47 } where 49 } where
48 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b } 50 prod-cong : ( a b : Obj (Sets {c₂}) ) {c : Obj (Sets {c₂}) } {f f' : Hom Sets c a } {g g' : Hom Sets c b }
49 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] 51 → Sets [ f ≈ f' ] → Sets [ g ≈ g' ]
50 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ] 52 → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
51 prod-cong a b {c} {f} {.f} {g} {.g} refl refl = refl 53 prod-cong a b {c} {f} {f1} {g} {g1} eq eq1 = ?
52 54
53 55
54 record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where 56 record iproduct {a} (I : Set a) ( pi0 : I → Set a ) : Set a where
55 field 57 field
56 pi1 : ( i : I ) → pi0 i 58 pi1 : ( i : I ) → pi0 i
72 } 74 }
73 } where 75 } where
74 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi) 76 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
75 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x } 77 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x }
76 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 ] 78 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 ]
77 pif=q {q} {qi} {i} = refl 79 pif=q {q} {qi} {i} = ?
78 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ] 80 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
79 ip-uniqueness = refl 81 ip-uniqueness = ?
80 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 82 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
81 ipcx {q} {qi} {qi'} qi=qi x = 83 ipcx {q} {qi} {qi'} qi=qi x =
82 begin 84 begin
83 record { pi1 = λ i → (qi i) x } 85 record { pi1 = λ i → (qi i) x }
84 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ? ⟩ -- ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩ 86 ≡⟨ ≡cong ( λ QIX → record { pi1 = QIX } ) ? ⟩ -- ( extensionality Sets (λ i → ≡cong ( λ f → f x ) (qi=qi i) )) ⟩
100 ; κ2 = λ i → k2 i 102 ; κ2 = λ i → k2 i
101 ; isProduct = record { 103 ; isProduct = record {
102 _+_ = sum 104 _+_ = sum
103 ; κ1f+g=f = ? -- extensionality Sets (λ x → refl ) 105 ; κ1f+g=f = ? -- extensionality Sets (λ x → refl )
104 ; κ2f+g=g = ? -- extensionality Sets (λ x → refl ) 106 ; κ2f+g=g = ? -- extensionality Sets (λ x → refl )
105 ; uniqueness = λ {c} {h} → extensionality Sets (λ x → uniq {c} {h} x ) 107 ; uniqueness = λ {c} {h} → ? -- extensionality Sets (λ x → uniq {c} {h} x )
106 ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → extensionality Sets (pccong feq geq) 108 ; +-cong = λ {c} {f} {f'} {g} {g'} feq geq → ? -- extensionality Sets (pccong feq geq)
107 } 109 }
108 } where 110 } where
109 sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c 111 sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c
110 sum {c} f g (k1 i) = f i 112 sum {c} f g (k1 i) = f i
111 sum {c} f g (k2 i) = g i 113 sum {c} f g (k2 i) = g i
133 } 135 }
134 } where 136 } where
135 isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q 137 isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q
136 isum {q} fi (ki1 i x) = fi i x 138 isum {q} fi (ki1 i x) = fi i x
137 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 ] 139 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 ]
138 kif=q {q} {qi} {i} = extensionality Sets (λ x → refl ) 140 kif=q {q} {qi} {i} = ? -- extensionality Sets (λ x → refl )
139 uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ] 141 uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ]
140 uniq {q} {h} = extensionality Sets u1 where 142 uniq {q} {h} = ? where -- extensionality Sets u1 where
141 u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x 143 u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x
142 u1 (ki1 i x) = refl 144 u1 (ki1 i x) = refl
143 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' ] 145 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' ]
144 iccong {q} {qi} {qi'} ieq = extensionality Sets u2 where 146 iccong {q} {qi} {qi'} ieq = ? where -- extensionality Sets u2 where
145 u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x 147 u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x
146 u2 (ki1 i x) = cong (λ k → k x ) (ieq i) 148 u2 (ki1 i x) = cong (λ k → k x ) ? -- (ieq i)
147 149
148 -- 150 --
149 -- e f 151 -- e f
150 -- c -------→ a ---------→ b f ( f' 152 -- c -------→ a ---------→ b f ( f'
151 -- ^ . ---------→ 153 -- ^ . ---------→
182 ; k = k 184 ; k = k
183 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq} 185 ; ek=h = λ {d} {h} {eq} → ek=h {d} {h} {eq}
184 ; uniqueness = uniqueness 186 ; uniqueness = uniqueness
185 } where 187 } where
186 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ] 188 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
187 fe=ge = extensionality Sets (fe=ge0 ) 189 fe=ge = ? -- extensionality Sets (fe=ge0 )
188 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) 190 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)
189 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) eq ) 191 k {d} h eq = λ x → elem (h x) ( ≡cong ( λ y → y x ) ? )
190 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 ] 192 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 ]
191 ek=h {d} {h} {eq} = refl 193 ek=h {d} {h} {eq} = ?
192 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂ 194 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂
193 injection f = ∀ x y → f x ≡ f y → x ≡ y 195 injection f = ∀ x y → f x ≡ f y → x ≡ y
194 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)} → 196 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)} →
195 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x) 197 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → (x : d ) → equ (k h fh=gh x) ≡ equ (k' x)
196 lemma5 refl x = refl -- somehow this is not equal to lemma1 198 lemma5 eq x = ? -- somehow this is not equal to lemma1
197 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)} → 199 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)} →
198 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ] 200 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
199 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ ( x : d ) → begin 201 uniqueness {d} {h} {fh=gh} {k'} ek'=h = ? -- extensionality Sets ( λ ( x : d ) → begin
200 k h fh=gh x 202 -- k h fh=gh x
201 ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩ 203 -- ≡⟨ elm-cong ( k h fh=gh x) ( k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) ⟩
202 k' x 204 -- k' x
203 ∎ ) where 205 -- ∎ ) where
204 open import Relation.Binary.PropositionalEquality 206 -- open import Relation.Binary.PropositionalEquality
205 open ≡-Reasoning 207 -- open ≡-Reasoning
206 208
207 209
208 -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c 210 -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c
209 -- record cequ {c : Level} (A B : Set c) : Set (suc c) where 211 -- record cequ {c : Level} (A B : Set c) : Set (suc c) where
210 -- field 212 -- field
315 ; isNTrans = record { commute = comm1 } 317 ; isNTrans = record { commute = comm1 }
316 } where 318 } where
317 comm1 : {a b : Obj C} {f : Hom C a b} → 319 comm1 : {a b : Obj C} {f : Hom C a b} →
318 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈ 320 Sets [ Sets [ FMap Γ f o (λ sn → snmap sn a) ] ≈
319 Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ] 321 Sets [ (λ sn → (snmap sn b)) o FMap (K C Sets (snat (ΓObj s Γ) (ΓMap s Γ))) f ] ]
320 comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin 322 comm1 {a} {b} {f} = ?
321 FMap Γ f (snmap sn a ) 323 -- comm1 {a} {b} {f} = extensionality Sets ( λ sn → begin
322 ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩ 324 -- FMap Γ f (snmap sn a )
323 FMap Γ ( hom← s ( hom→ s f)) (snmap sn a ) 325 -- ≡⟨ ≡cong ( λ f → ( FMap Γ f (snmap sn a ))) (sym ( ≡←≈ s ( hom-iso s ))) ⟩
324 ≡⟨⟩ 326 -- FMap Γ ( hom← s ( hom→ s f)) (snmap sn a )
325 ΓMap s Γ (hom→ s f) (snmap sn a ) 327 -- ≡⟨⟩
326 ≡⟨ sncommute sn a b (hom→ s f) ⟩ 328 -- ΓMap s Γ (hom→ s f) (snmap sn a )
327 snmap sn b 329 -- ≡⟨ sncommute sn a b (hom→ s f) ⟩
328 ∎ ) where 330 -- snmap sn b
329 open import Relation.Binary.PropositionalEquality 331 -- ∎ ) where
330 open ≡-Reasoning 332 -- open import Relation.Binary.PropositionalEquality
331 333 -- open ≡-Reasoning
334 --
332 335
333 SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 336 SetsLimit : { c₁ c₂ ℓ : Level} ( I : Set c₁ ) ( C : Category c₁ c₂ ℓ ) ( small : Small C I ) ( Γ : Functor C (Sets {c₁} ) )
334 → Limit C Sets Γ 337 → Limit C Sets Γ
335 SetsLimit {c₁} I C s Γ = record { 338 SetsLimit {c₁} I C s Γ = record {
336 a0 = snat (ΓObj s Γ) (ΓMap s Γ) 339 a0 = snat (ΓObj s Γ) (ΓMap s Γ)