Mercurial > hg > Members > kono > Proof > category

annotate SetsCompleteness.agda @ 518:52d30ad7f652

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 21 Mar 2017 15:15:46 +0900
parents 6f7630a255e4
children 844328b49d5d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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 HomReasoning
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import cat-utility
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 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
12 open import Function
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
13 import Relation.Binary.PropositionalEquality
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
14 -- 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
15 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
16
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
17 ≡-cong = Relation.Binary.PropositionalEquality.cong
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
18
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
19
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
20
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
21 record Σ {a} (A : Set a) (B : Set a) : Set a where
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
22 constructor _,_
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
23 field
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
24 proj₁ : A
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
25 proj₂ : B
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
26
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
27 open Σ public
500
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
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 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
31 SetsProduct { c₂ } = record {
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
32 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
33 ; π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
34 ; π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
35 ; isProduct = λ a b → record {
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
36 _×_ = λ 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
37 ; π1fxg=f = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 ; π2fxg=g = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; uniqueness = refl
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ; ×-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
41 }
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 } where
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 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
44 → 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
45 → 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
46 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
47
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
49 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
50 field
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
51 pi1 : ( i : I ) → pi0 i
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
52
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
53 open iproduct
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
54
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
55 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
56 → IProduct ( Sets { c₂} ) I
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
57 SetsIProduct I fi = record {
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
58 ai = fi
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
59 ; iprod = iproduct I fi
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
60 ; pi = λ i prod → pi1 prod i
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
61 ; isIProduct = record {
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
62 iproduct = iproduct1
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
63 ; pif=q = pif=q
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
64 ; ip-uniqueness = ip-uniqueness
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
65 ; ip-cong = ip-cong
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
66 }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
67 } where
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
68 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
69 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
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 ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
71 pif=q {q} qi {i} = refl
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
72 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
73 ip-uniqueness = refl
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
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
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
75 ipcx {q} {qi} {qi'} qi=qi x =
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
76 begin
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
77 record { pi1 = λ i → (qi i) x }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
78 ≡⟨ ≡-cong ( λ QIX → record { pi1 = QIX } ) ( extensionality Sets (λ i → ≡-cong ( λ f → f x ) (qi=qi i) )) ⟩
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
79 record { pi1 = λ i → (qi' i) x }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
80 ∎ where
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
81 open import Relation.Binary.PropositionalEquality
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
82 open ≡-Reasoning
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
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' ]
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
84 ip-cong {q} {qi} {qi'} qi=qi = extensionality Sets ( ipcx qi=qi )
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
85
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
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
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
89 -- c -------→ a ---------→ b f ( f'
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
90 -- ^ . ---------→
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
514
1fca61019bdf on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 513
diff changeset
94 --y : d
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
95
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
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
100 open sequ
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
101
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
102 SetsEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → Equalizer Sets f g
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
103 SetsEqualizer {c₂} a b f g = record {
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
104 equalizer-c = sequ a b f g
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
105 ; equalizer = λ e → equ e
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 ; isEqualizer = record {
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
107 fe=ge = fe=ge
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
108 ; k = k
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
109 ; 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
110 ; uniqueness = uniqueness
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 }
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
112 } where
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
113 equ : ( sequ a b f g ) → a
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
114 equ (elem x eq) = x
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
115 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
116 fe=ge0 (elem x eq ) = eq
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
117 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
118 fe=ge = extensionality Sets (fe=ge0 )
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
119 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)
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
120 k {d} h eq = λ x → elem (h x) ( cong ( λ y → y x ) eq )
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
121 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
122 ek=h {d} {h} {eq} = refl
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
123 fhy=ghy : (d : Obj Sets ) ( h : Hom Sets d a ) (y : d ) → (fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]) → f (h y) ≡ g (h y)
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
124 fhy=ghy d h y fh=gh = cong ( λ f → f y ) fh=gh
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
125 xequ : (x : a ) → { fx=gx : f x ≡ g x } → sequ a b f g
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
126 xequ x { fx=gx } = elem x fx=gx
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
127 lemma1 : ( e : sequ a b f g ) → ( z : sequ a b f g ) → elem (equ z) (fe=ge0 z) ≡ z
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
128 lemma1 ( elem x eq ) (elem x' eq' ) = refl
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
129 lemma2 : { e : sequ a b f g } → ( λ e → elem (equ e) (fe=ge0 e ) ) ≡ ( λ e → e )
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
130 lemma2 {e} = extensionality Sets ( λ z → lemma1 e z )
518
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
131 lemma3 : {d : Obj Sets} ( e : sequ a b f g → a ) → ( y : d ) → (k' : Hom Sets d (sequ a b f g)) → f ( e (k' y) ) ≡ g ( e (k' y))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
132 lemma3 {d} e y k' = {!!}
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
133 uniquness1 : {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)} → ( y : d ) →
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
134 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → k h fh=gh y ≡ k' y
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
135 uniquness1 {d} {h} {fh=gh} {k'} y ek'=h =
511
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
136 begin
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
137 k h fh=gh y
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
138 ≡⟨⟩
513
e73c3e73a87b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 512
diff changeset
139 elem (h y) (fhy=ghy d h y fh=gh )
514
1fca61019bdf on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 513
diff changeset
140 ≡⟨⟩
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
141 xequ (h y ) {fhy=ghy d h y fh=gh }
518
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
142 ≡⟨ sym ( Category.cong (λ ek' → xequ (ek' y ) {{!!}} ) ek'=h ) ⟩
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
143 xequ ( ( λ e → equ e ) ( k' y ) ) {fe=ge0 (k' y)}
513
e73c3e73a87b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 512
diff changeset
144 ≡⟨⟩
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
145 ( λ e → xequ ( equ e ) {fe=ge0 e } ) ( k' y )
515
221dd46ded35 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 514
diff changeset
146 ≡⟨⟩
221dd46ded35 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 514
diff changeset
147 ( λ e → elem (equ e) (fe=ge0 e )) ( k' y )
516
327dc7372729 yellow remains ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 515
diff changeset
148 ≡⟨ Category.cong ( λ f → f ( k' y ) ) lemma2 ⟩
515
221dd46ded35 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 514
diff changeset
149 ( λ e → e ) ( k' y )
221dd46ded35 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 514
diff changeset
150 ≡⟨⟩
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
151 k' y
511
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
152 ∎
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
153 where
511
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
154 open import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
155 open ≡-Reasoning
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
156 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)} →
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
157 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
517
6f7630a255e4 on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 516
diff changeset
158 uniqueness {d} {h} {fh=gh} {k'} ek'=h = extensionality Sets ( λ y → uniquness1 {d} {h} {fh=gh}{k'} y ek'=h )
518
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
159 uniqueness0 : {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)} →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
160 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
161 uniqueness0 {d} {h} {fh=gh} {k'} ek'=h = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
162 k h fh=gh
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
163 ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
164 k ( Sets [ (λ e → equ e) o k' ] ) {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
165 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
166 Sets [ ( λ e → elem (equ e) (fe=ge0 e )) o k' ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
167 ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
168 Sets [ ( λ e → e ) o k' ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
169 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
170 k'
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
171 ∎ where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
172 open ≈-Reasoning Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 517
diff changeset
173
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
174
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175
501
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
176 open Functor
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
177 open NTrans
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
179
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
180
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
181 record ΓObj { c₂ } ( I : Set c₂ ) : Set c₂ where
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
182 field
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
183 obj : I
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
184
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
185 open ΓObj
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
186
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
187 record ΓMap { c₂ } {a b : Set c₂ } ( f : a → b ) : Set c₂ where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
188 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
189 map : ΓObj a → ΓObj b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
190
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
191 open ΓMap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
192
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
193 fmap : { c₂ : Level} {a b : Set c₂ } → (f : a → b ) → ΓMap f
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
194 fmap {a} {b} f = record { map = λ aobj → record { obj = f ( obj aobj ) } }
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
195
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
196 Γ : { c₂ : Level } → Functor (Sets { c₂}) (Sets { c₂})
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
197 Γ { c₂} = record { FObj = ΓObj ; FMap = ( λ f → map (fmap f )) ; isFunctor = record {
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
198 identity = λ {b} → refl ;
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
199 distr = λ {a} {b} {c} {f} {g} → refl ;
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
200 ≈-cong = cong1
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
201 } } where
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
202 cong1 : {A B : Obj Sets} {f g : Hom Sets A B} → Sets [ f ≈ g ] → Sets [ map (fmap f) ≈ map (fmap g) ]
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
203 cong1 refl = refl
507
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
204
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 506
diff changeset
205
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
206 record Slimit { c₂ } (I : Set c₂) ( sobj : I → Set c₂ ) (smap : { a b : Set c₂ } ( f : a → b ) → Set c₂ )
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
207 : Set c₂ where
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
208 field
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
209 sm : I → I
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
210 s-t0 : (i : I ) → sobj i
501
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
211
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
212 open Slimit
61daa68a70c4 Sets completeness failed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
213
511
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
214 -- SetsLimit : { c₂ : Level} → Limit Sets Sets Γ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
215 -- SetsLimit { c₂} = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
216 -- a0 = Slimit (Obj Sets) {!!} ΓMap
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
217 -- ; t0 = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
218 -- TMap = λ i → λ lim → s-t0 lim {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
219 -- ; isNTrans = record { commute = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
220 -- }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
221 -- ; isLimit = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
222 -- limit = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
223 -- ; t0f=t = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
224 -- ; limit-uniqueness = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
225 -- }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 510
diff changeset
226 -- } where
508
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
227 -- comm1 : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → s-t0 lim ? ) ] ≈
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
228 -- Sets [ (λ lim → s-t0 lim ?) o FMap (K Sets Sets (Slimit (Obj Sets) ΓObj (λ {a} {b} → ΓMap))) f ] ]
3ce21b2a671a IProduct is written in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 507
diff changeset
229 -- comm1 {a} {b} {f} = {!!}