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