Mercurial > hg > Members > kono > Proof > category

annotate src/SetsCompleteness.agda @ 1124:f683d96fbc93 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
safe fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2024 22:28:50 +0900
parents 5620d4a85069
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
1 {-# OPTIONS --cubical-compatible --safe #-}
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1034
diff changeset
2
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
3 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
4 open import Level
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
5 open import Category.Sets
500
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 module SetsCompleteness where
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
1110
45de2b31bf02 add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1034
diff changeset
9 open import Definitions
500
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
781
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 693
diff changeset
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
340708e8d54f fix for 2.5.4.2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 693
diff changeset
15
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
16 lemma1 : { c₂ : Level } {a b : Obj (Sets { c₂})} {f g : Hom Sets a b} →
524
d6739779b4ac on going ..
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 523
diff changeset
17 Sets [ f ≈ g ] → (x : a ) → f x ≡ g x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
18 lemma1 eq x = eq x
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
19
504
b489f27317fb on going...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 503
diff changeset
20 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
21 constructor _,_
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
22 field
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
23 proj₁ : A
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
24 proj₂ : B
503
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
25
bd33096c189b on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 501
diff changeset
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
681
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
29 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
30 SetsProduct { c₂ } a b = record {
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
31 product = Σ a b
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
32 ; π1 = λ ab → (proj₁ ab)
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
33 ; π2 = λ ab → (proj₂ ab)
bd8f7346f252 fix Product and pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 676
diff changeset
34 ; isProduct = record {
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
35 _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x )
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
36 ; π1fxg=f = λ {c} {f} {g} x → refl
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
37 ; π2fxg=g = λ {c} {f} {g} x → refl
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
38 ; uniqueness = λ {c} {h} x → refl
500
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) ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
45 prod-cong a b {c} {f} {f1} {g} {g1} eq eq1 x = cong₂ (λ j k → j , k) (eq x) (eq1 x)
500
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
52 open iproduct
574
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 573
diff changeset
53
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
54 open Small
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
55
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
56 open import Axiom.Extensionality.Propositional
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
57
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
58 SetsIProduct : { c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
1124
f683d96fbc93 safe fix done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1115
diff changeset
59 → Extensionality c₂ c₂ -- cannot avoid this here
691
917e51be9bbf change argument of Limit and K
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 681
diff changeset
60 → IProduct I ( Sets { c₂} ) ai
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
61 SetsIProduct {c₂} I fi ext = record {
673
0007f9a25e9c fix limit from product and equalizer (not yet finished )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 672
diff changeset
62 iprod = iproduct I fi
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
63 ; pi = λ i prod → pi1 prod i
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
64 ; isIProduct = record {
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
65 iproduct = iproduct1
676
faf48511f69d two product as in CWM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 673
diff changeset
66 ; pif=q = λ {q} {qi} {i} → pif=q {q} {qi} {i}
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
67 ; ip-uniqueness = ip-uniqueness
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
68 ; ip-cong = ip-cong
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
69 }
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
70 } where
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
71 iproduct1 : {q : Obj Sets} → ((i : I) → Hom Sets q (fi i)) → Hom Sets q (iproduct I fi)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
72 iproduct1 {q} qi x = record { pi1 = λ i → (qi i) x }
676
faf48511f69d two product as in CWM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 673
diff changeset
73 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 ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
74 pif=q {q} {qi} {i} x = refl
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
75 ip-uniqueness : {q : Obj Sets} {h : Hom Sets q (iproduct I fi)} → Sets [ iproduct1 (λ i → Sets [ (λ prod → pi1 prod i) o h ]) ≈ h ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
76 ip-uniqueness {q} {h} x = refl
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
77 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
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
78 ipcx {q} {qi} {qi'} qi=qi x =
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
79 begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
80 record { pi1 = λ i → (qi i) x }
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
81 ≡⟨ cong (λ k → record { pi1 = k} ) (ext (λ i → qi=qi i x) ) ⟩
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
82 record { pi1 = λ i → (qi' i) x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
83 ∎ where
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
84 open import Relation.Binary.PropositionalEquality
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
85 open ≡-Reasoning
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
86 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' ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
87 ip-cong {q} {qi} {qi'} qi=qi = ipcx qi=qi
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
88
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
89 data coproduct {c} (a b : Set c) : Set c where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
90 k1 : ( i : a ) → coproduct a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
91 k2 : ( i : b ) → coproduct a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
92
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
93 SetsCoProduct : { c₂ : Level} → (a b : Obj (Sets {c₂})) → coProduct Sets a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
94 SetsCoProduct a b = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
95 coproduct = coproduct a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
96 ; κ1 = λ i → k1 i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
97 ; κ2 = λ i → k2 i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
98 ; isProduct = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
99 _+_ = sum
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
100 ; κ1f+g=f = λ {c} {f} {g} x → fk1 {c} {f} {g} x
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
101 ; κ2f+g=g = λ {c} {f} {g} x → fk2 {c} {f} {g} x
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
102 ; uniqueness = λ {c} {h} x → uniq {c} {h} x
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
103 ; +-cong = pccong
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
104 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
105 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
106 sum : {c : Obj Sets} → Hom Sets a c → Hom Sets b c → Hom Sets (coproduct a b ) c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
107 sum {c} f g (k1 i) = f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
108 sum {c} f g (k2 i) = g i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
109 uniq : {c : Obj Sets} {h : Hom Sets (coproduct a b) c} → (x : coproduct a b ) → sum (Sets [ h o (λ i → k1 i) ]) (Sets [ h o (λ i → k2 i) ]) x ≡ h x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
110 uniq {c} {h} (k1 i) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
111 uniq {c} {h} (k2 i) = refl
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
112 pccong : {c : Obj Sets} {f f' : Hom Sets a c} {g g' : Hom Sets b c} → Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ sum f g ≈ sum f' g' ]
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
113 pccong {c} {f} {f'} {g} {g'} eq eq1 (k1 i) = eq i
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
114 pccong {c} {f} {f'} {g} {g'} eq eq1 (k2 i) = eq1 i
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
115 fk1 : {c : Obj Sets} {f : Hom Sets a c} {g : Hom Sets b c} → Sets [ Sets [ sum f g o (λ i → k1 i) ] ≈ f ]
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
116 fk1 {c} {f} {g} x = refl
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
117 fk2 : {c : Obj Sets} {f : Hom Sets a c} {g : Hom Sets b c} → Sets [ Sets [ sum f g o (λ i → k2 i) ] ≈ g ]
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
118 fk2 {c} {f} {g} x = refl
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
119
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
120
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
121 data icoproduct {a} (I : Set a) (ki : I → Set a) : Set a where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
122 ki1 : (i : I) (x : ki i ) → icoproduct I ki
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
123
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
124 SetsICoProduct : { c₂ : Level} → (I : Obj (Sets {c₂})) (ci : I → Obj Sets )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
125 → ICoProduct I ( Sets { c₂} ) ci
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
126 SetsICoProduct I fi = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
127 icoprod = icoproduct I fi
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
128 ; ki = λ i x → ki1 i x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
129 ; isICoProduct = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
130 icoproduct = isum
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
131 ; kif=q = λ {q} {qi} {i} → kif=q {q} {qi} {i}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
132 ; icp-uniqueness = uniq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
133 ; icp-cong = iccong
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
134 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
135 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
136 isum : {q : Obj Sets} → ((i : I) → Hom Sets (fi i) q) → Hom Sets (icoproduct I fi) q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
137 isum {q} fi (ki1 i x) = fi i x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
138 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 ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
139 kif=q {q} {qi} {i} x = refl
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
140 uniq : {q : Obj Sets} {h : Hom Sets (icoproduct I fi) q} → Sets [ isum (λ i → Sets [ h o (λ x → ki1 i x) ]) ≈ h ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
141 uniq {q} {h} = u1 where
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
142 u1 : (x : icoproduct I fi ) → isum (λ i → Sets [ h o (λ x₁ → ki1 i x₁) ]) x ≡ h x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
143 u1 (ki1 i x) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
144 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' ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
145 iccong {q} {qi} {qi'} ieq = u2 where
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
146 u2 : (x : icoproduct I fi ) → isum qi x ≡ isum qi' x
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
147 u2 (ki1 i x) = ieq i x
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
148
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
149 --
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
150 -- e f
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
151 -- c -------→ a ---------→ b f ( f'
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
152 -- ^ . ---------→
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
153 -- | . g
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
154 -- |k .
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
155 -- | . h
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
156 --y : d
509
3e82fb1ce170 IProduct in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 508
diff changeset
157
522
8fd030f9f572 Equalizer in Sets done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 521
diff changeset
158 -- 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
159
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
160 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
161 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
162
532
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
163 equ : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } → ( sequ a b f g ) → a
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
164 equ (elem x eq) = x
532
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
165
606
92eb707498c7 fix for new agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 605
diff changeset
166 fe=ge0 : { c₂ : Level} {a b : Obj (Sets {c₂}) } { f g : Hom (Sets {c₂}) a b } →
533
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
167 (x : sequ a b f g) → (Sets [ f o (λ e → equ e) ]) x ≡ (Sets [ g o (λ e → equ e) ]) x
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
168 fe=ge0 (elem x eq ) = eq
c3dcea3a92a7 use sequ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 532
diff changeset
169
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
170 -- we need -with-K to prove this
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
171 --- ≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq'
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
172
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
173 equ-inject : { c₂ : Level} {a b : Set c₂}
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
174 (≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq')
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
175 {f g : Hom (Sets {c₂}) a b} (x y : sequ a b f g) → equ x ≡ equ y → x ≡ y
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
176 equ-inject ≡-irr ( elem x eq ) (elem .x eq' ) refl = cong (λ k → elem x k ) (≡-irr eq eq' )
541
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 540
diff changeset
177
510
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
178 open sequ
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
179
532
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
180 -- equalizer-c = sequ a b f g
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
181 -- ; equalizer = λ e → equ e
d5d7163f2a1d equalizer does not fit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 531
diff changeset
182
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
183 open import Relation.Binary.PropositionalEquality
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
184
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
185 SetsIsEqualizer : { c₂ : Level}
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
186 (≡-irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq')
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
187 → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
188 SetsIsEqualizer {c₂} ≡-irr a b f g = record {
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
189 fe=ge = fe=ge
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
190 ; k = k
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
191 ; 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
192 ; uniqueness = uniqueness
5eb4b69bf541 equalizer in Sets , uniquness remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 509
diff changeset
193 } where
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
194 fe=ge : Sets [ Sets [ f o (λ e → equ e ) ] ≈ Sets [ g o (λ e → equ e ) ] ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
195 fe=ge (elem x eq) = eq
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
196 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)
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
197 k {d} h eq x = elem (h x) (eq x)
604
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 603
diff changeset
198 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 ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
199 ek=h {d} {h} {eq} x = refl
523
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
200 injection : { c₂ : Level } {a b : Obj (Sets { c₂})} (f : Hom Sets a b) → Set c₂
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 522
diff changeset
201 injection f = ∀ x y → f x ≡ f y → x ≡ y
512
f19dab948e39 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 511
diff changeset
202 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
203 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh ≈ k' ]
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
204 uniqueness {d} {h} {fh=gh} {k'} ek'=h x = equ-inject ≡-irr _ _ ( begin
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
205 equ ( k h fh=gh x) ≡⟨⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
206 h x ≡⟨ sym ( ek'=h x) ⟩
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
207 equ (k' x) ∎ ) where open ≡-Reasoning
999
d89f2c8cf0f4 separate CCCSets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 998
diff changeset
208
1009
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
209 -- -- we have to make this Level c, that is {B : Set c} → (A → B) is iso to I : Set c
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
210 -- record cequ {c : Level} (A B : Set c) : Set (suc c) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
211 -- field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
212 -- rev : {B : Set c} → (A → B) → B → A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
213 -- surjective : {B : Set c } (x : B ) → (g : A → B) → g (rev g x) ≡ x
999
d89f2c8cf0f4 separate CCCSets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 998
diff changeset
214
1009
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
215 -- -- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
216 -- -- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
217 -- -- Y / R
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
218
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
219 -- open import HomReasoning
986
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 949
diff changeset
220
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
221 -- SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b)
1009
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
222 -- → IsCoEqualizer Sets (λ x → {!!} ) f g
1115
5620d4a85069 safe rewriting nearly finished
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1112
diff changeset
223 -- SetsIsCoEqualizer {c₂} a b f g = record {
1009
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
224 -- ef=eg = extensionality Sets (λ x → {!!} )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
225 -- ; k = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
226 -- ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
227 -- ; uniqueness = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
228 -- } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
229 -- c : Set c₂
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
230 -- c = {!!} --cequ a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
231 -- d : cequ a b
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
232 -- d = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
233 -- ef=eg : Sets [ Sets [ cequ.rev d f o f ] ≈ Sets [ cequ.rev d g o g ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
234 -- ef=eg = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
235 -- Sets [ cequ.rev d f o f ] ≈↑⟨ idL ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
236 -- Sets [ id1 Sets _ o Sets [ cequ.rev d f o f ] ] ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
237 -- Sets [ Sets [ id1 Sets _ o cequ.rev d f ] o f ] ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
238 -- Sets [ Sets [ id1 Sets _ o cequ.rev d (id1 Sets _) ] o {!!} ] ≈⟨ car ( extensionality Sets (λ x → cequ.surjective d {!!} {!!} )) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
239 -- Sets [ {!!} o f ] ≈⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
240 -- Sets [ id1 Sets _ o Sets [ cequ.rev d g o g ] ] ≈⟨ idL ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
241 -- Sets [ cequ.rev d g o g ] ∎ where open ≈-Reasoning Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
242 -- epi : { c₂ : Level } {a b c : Obj (Sets { c₂})} (e : Hom Sets b c ) → (f g : Hom Sets a b) → Set c₂
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
243 -- epi e f g = Sets [ Sets [ e o f ] ≈ Sets [ e o g ] ] → Sets [ f ≈ g ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
244 -- k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
245 -- k {d} h hf=hg = {!!} where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
246 -- ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
247 -- ca eq = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
248 -- cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
249 -- cd = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
250 -- ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
251 -- → Sets [ Sets [ k h eq o {!!} ] ≈ h ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
252 -- ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
253 -- k h eq ( {!!}) ≡⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
254 -- h (f {!!}) ≡⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
255 -- h (g {!!}) ≡⟨ {!!} ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
256 -- h x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
257 -- ∎ ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
258 -- open import Relation.Binary.PropositionalEquality
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1008
diff changeset
259 -- open ≡-Reasoning
997
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 987
diff changeset
260
500
6c993c1fe9de try to make prodcut and equalizer in Sets
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
261