annotate equalizer.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Apr 2019 23:42:19 +0900
parents f526f4b68565
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
205
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 ---
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 --
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 -- Equalizer
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 --
208
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 207
diff changeset
5 -- e f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
6 -- c -------→ a ---------→ b
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
7 -- ^ . ---------→
205
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 -- | . g
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
9 -- |k .
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
10 -- | . h
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
11 -- d
205
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 --
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ----
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
16 open import Category -- https://github.com/konn/category-agda
205
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Level
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open import HomReasoning
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open import cat-utility
242adb6669da equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
260
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
23 -- in cat-utility
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
24 -- record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
25 -- field
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
26 -- fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ]
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
27 -- k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
28 -- ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ]
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
29 -- uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
30 -- A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ]
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
31 -- equalizer : Hom A c a
a87d3ea9efe4 pullback
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 259
diff changeset
32 -- equalizer = e
206
3a5e2a22e053 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 205
diff changeset
33
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
34
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
35 --
251
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
36 -- Burroni's Flat Equational Definition of Equalizer
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
37 --
236
e20b81102eee Burroni equational equalizer definition done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
38 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) (e : Hom A c a) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
206
3a5e2a22e053 on going
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 205
diff changeset
39 field
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
40 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (e : Hom A c a ) → Hom A c a
214
f8afdb9ed99a b4 remains.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
41 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
42 δ : {a b c : Obj A } → (e : Hom A c a ) → (f : Hom A a b) → Hom A a c
242
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 241
diff changeset
43 cong-α : {a b c : Obj A } → { e : Hom A c a }
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
44 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ α f g e ≈ α f g' e ]
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
45 cong-γ : {a _ c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ]
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
46 → A [ γ {a} {b} {c} {d} f g h ≈ γ f g h' ]
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
47 cong-δ : {a b c : Obj A } → {e : Hom A c a} → {f f' : Hom A a b} → A [ f ≈ f' ] → A [ δ e f ≈ δ e f' ]
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
48 b1 : A [ A [ f o α {a} {b} {c} f g e ] ≈ A [ g o α {a} {b} {c} f g e ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
49 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α {a} {b} {c} f g e ) o (γ {a} {b} {c} f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) (id1 A d) ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
50 b3 : {a b d : Obj A} → (f : Hom A a b ) → {h : Hom A d a } → A [ A [ α {a} {b} {d} f f h o δ {a} {b} {d} h f ] ≈ id1 A a ]
207
22811f7a04e1 Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 206
diff changeset
51 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ]
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
52 b4 : {d : Obj A } {k : Hom A d c} →
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
53 A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g e o k ] ) o ( δ {d} {b} {d} (id1 A d) (A [ f o A [ α {a} {b} {c} f g e o k ] ] ) )] ≈ k ]
207
22811f7a04e1 Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 206
diff changeset
54 -- A [ α f g o β f g h ] ≈ h
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
55 β : { d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
56 β {d} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ {d} {b} {d} (id1 A d) (A [ f o h ]) ]
207
22811f7a04e1 Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 206
diff changeset
57
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
58
209
4e138cc953f3 equalizer difinition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 208
diff changeset
59 open Equalizer
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
60 open IsEqualizer
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
61 open Burroni
209
4e138cc953f3 equalizer difinition
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 208
diff changeset
62
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
63 --
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
64 -- Some obvious conditions for k (fe = ge) → ( fh = gh )
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
65 --
219
2ae029454fb6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
66
224
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
67 f1=g1 : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → (h : Hom A c a) → A [ A [ f o h ] ≈ A [ g o h ] ]
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
68 f1=g1 eq h = let open ≈-Reasoning (A) in (resp refl-hom eq )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
69
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
70 f1=f1 : { a b : Obj A } (f : Hom A a b ) → A [ A [ f o (id1 A a) ] ≈ A [ f o (id1 A a) ] ]
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
71 f1=f1 f = let open ≈-Reasoning (A) in refl-hom
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
72
224
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
73 f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
74 (eq : A [ A [ f o e ] ≈ A [ g o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e o h ] ] ]
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
75 f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in
224
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
76 begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
77 f o ( e o h )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
78 ≈⟨ assoc ⟩
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
79 (f o e ) o h
224
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
80 ≈⟨ car eq ⟩
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
81 (g o e ) o h
224
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
82 ≈↑⟨ assoc ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
83 g o ( e o h )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 223
diff changeset
84
219
2ae029454fb6 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 218
diff changeset
85
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
86 -------------------------------
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
87 --
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
88 -- Every equalizer is monic
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
89 --
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
90 -- e i = e j → i = j
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
91 --
259
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
92 -- e eqa f g f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
93 -- c ---------→ a ------→b
259
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
94 -- ^^
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
95 -- ||
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
96 -- i||j
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
97 -- ||
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
98 -- d
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
99
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
100 monoic : { c a b d : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A f g)
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
101 → { i j : Hom A d (equalizer-c eqa) }
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
102 → A [ A [ equalizer eqa o i ] ≈ A [ equalizer eqa o j ] ] → A [ i ≈ j ]
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
103 monoic {c} {a} {b} {d} {f} {g} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
104 i
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
105 ≈↑⟨ uniqueness (isEqualizer eqa) ( begin
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
106 equalizer eqa o i
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
107 ≈⟨ ei=ej ⟩
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
108 equalizer eqa o j
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
109 ∎ )⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
110 k (isEqualizer eqa) (equalizer eqa o j) ( f1=gh (fe=ge (isEqualizer eqa) ) )
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
111 ≈⟨ uniqueness (isEqualizer eqa) ( begin
257
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 256
diff changeset
112 equalizer eqa o j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 256
diff changeset
113 ≈⟨⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 256
diff changeset
114 equalizer eqa o j
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 256
diff changeset
115 ∎ )⟩
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
116 j
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
117
255
7e7b2c38dee1 every equalizer is monic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
118
251
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
119 --------------------------------
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
120 --
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
121 --
259
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
122 -- Isomorphic arrows from c' to c makes another equalizer
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
123 --
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
124 -- e eqa f g f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
125 -- c ---------→ a ------→b
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
126 -- |^
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
127 -- ||
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
128 -- h || h-1
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
129 -- v|
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
130 -- c'
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
131
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
132 equalizer+iso : {a b c' : Obj A } {f g : Hom A a b } →
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
133 ( eqa : Equalizer A f g ) →
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
134 (h-1 : Hom A c' (equalizer-c eqa) ) → (h : Hom A (equalizer-c eqa) c' ) →
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
135 A [ A [ h o h-1 ] ≈ id1 A c' ] → A [ A [ h-1 o h ] ≈ id1 A (equalizer-c eqa) ]
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
136 → IsEqualizer A (A [ equalizer eqa o h-1 ] ) f g
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
137 equalizer+iso {a} {b} {c'} {f} {g} eqa h-1 h hh-1=1 h-1h=1 = record {
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
138 fe=ge = fe=ge1 ;
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
139 k = λ j eq → A [ h o k (isEqualizer eqa) j eq ] ;
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
140 ek=h = ek=h1 ;
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
141 uniqueness = uniqueness1
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
142 } where
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
143 e = equalizer eqa
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
144 fe=ge1 : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [ e o h-1 ] ] ]
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
145 fe=ge1 = f1=gh ( fe=ge (isEqualizer eqa) )
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
146 ek=h1 : {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
147 A [ A [ A [ e o h-1 ] o A [ h o k (isEqualizer eqa) j eq ] ] ≈ j ]
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
148 ek=h1 {d} {j} {eq} = let open ≈-Reasoning (A) in
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
149 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
150 ( e o h-1 ) o ( h o k (isEqualizer eqa) j eq )
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
151 ≈↑⟨ assoc ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
152 e o ( h-1 o ( h o k (isEqualizer eqa) j eq ) )
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
153 ≈⟨ cdr assoc ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
154 e o (( h-1 o h) o k (isEqualizer eqa) j eq )
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
155 ≈⟨ cdr (car h-1h=1 ) ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
156 e o (id1 A (equalizer-c eqa) o k (isEqualizer eqa) j eq )
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
157 ≈⟨ cdr idL ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
158 e o k (isEqualizer eqa) j eq
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
159 ≈⟨ ek=h (isEqualizer eqa) ⟩
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
160 j
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
161
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
162 uniqueness1 : {d : Obj A} {h' : Hom A d a} {eq : A [ A [ f o h' ] ≈ A [ g o h' ] ]} {j : Hom A d c'} →
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
163 A [ A [ A [ e o h-1 ] o j ] ≈ h' ] →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
164 A [ A [ h o k (isEqualizer eqa) h' eq ] ≈ j ]
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
165 uniqueness1 {d} {h'} {eq} {j} ej=h = let open ≈-Reasoning (A) in
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
166 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
167 h o k (isEqualizer eqa) h' eq
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
168 ≈⟨ cdr (uniqueness (isEqualizer eqa) ( begin
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
169 e o ( h-1 o j )
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
170 ≈⟨ assoc ⟩
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
171 (e o h-1 ) o j
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
172 ≈⟨ ej=h ⟩
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
173 h'
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
174 ∎ )) ⟩
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
175 h o ( h-1 o j )
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
176 ≈⟨ assoc ⟩
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
177 (h o h-1 ) o j
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
178 ≈⟨ car hh-1=1 ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
179 id c' o j
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
180 ≈⟨ idL ⟩
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
181 j
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
182
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
183
251
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
184 --------------------------------
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
185 --
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
186 -- If we have two equalizers on c and c', there are isomorphic pair h, h'
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
187 --
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
188 -- h : c → c' h' : c' → c
233
4bba19bc71be e is now explict parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 232
diff changeset
189 -- e' = h o e
4bba19bc71be e is now explict parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 232
diff changeset
190 -- e = h' o e'
259
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
191 --
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
192 --
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
193 --
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
194 -- e eqa f g f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
195 -- c ---------→a ------→b
259
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
196 -- ^ ^ g
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
197 -- | |
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
198 -- |k = id c' |
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
199 -- v |
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
200 -- c'-----------+
c442322d22b3 add figure
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 258
diff changeset
201 -- e eqa' f g
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
202
233
4bba19bc71be e is now explict parameter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 232
diff changeset
203 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a }
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
204 ( eqa : IsEqualizer A e f g) → ( eqa' : IsEqualizer A e' f g )
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
205 → Hom A c c'
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
206 c-iso-l {c} {c'} {a} {b} {f} {g} {e} eqa eqa' = k eqa' e ( fe=ge eqa )
223
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 222
diff changeset
207
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
208 c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a }
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
209 ( eqa : IsEqualizer A e f g) → ( eqa' : IsEqualizer A e' f g )
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
210 → Hom A c' c
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
211 c-iso-r {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' = k eqa e' ( fe=ge eqa' )
228
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 227
diff changeset
212
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
213 c-iso-lr : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } { e' : Hom A c' a }
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
214 ( eqa : IsEqualizer A e f g) → ( eqa' : IsEqualizer A e' f g ) →
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
215 A [ A [ c-iso-l eqa eqa' o c-iso-r eqa eqa' ] ≈ id1 A c' ]
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
216 c-iso-lr {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' = let open ≈-Reasoning (A) in begin
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
217 c-iso-l eqa eqa' o c-iso-r eqa eqa'
250
a1e2228c2a6b equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 249
diff changeset
218 ≈⟨⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
219 k eqa' e ( fe=ge eqa ) o k eqa e' ( fe=ge eqa' )
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
220 ≈↑⟨ uniqueness eqa' ( begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
221 e' o ( k eqa' e (fe=ge eqa) o k eqa e' (fe=ge eqa') )
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
222 ≈⟨ assoc ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
223 ( e' o k eqa' e (fe=ge eqa) ) o k eqa e' (fe=ge eqa')
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
224 ≈⟨ car (ek=h eqa') ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
225 e o k eqa e' (fe=ge eqa')
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
226 ≈⟨ ek=h eqa ⟩
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
227 e'
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
228 ∎ )⟩
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
229 k eqa' e' ( fe=ge eqa' )
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
230 ≈⟨ uniqueness eqa' ( begin
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
231 e' o id c'
250
a1e2228c2a6b equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 249
diff changeset
232 ≈⟨ idR ⟩
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
233 e'
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
234 ∎ )⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
235 id c'
229
68b2681ea9df c in equalizer is equal up to iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
236
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
237
258
281b8962abbe simpler equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
238 -- c-iso-rl is obvious from the symmetry
234
c02287d3d2dc equalizer iso done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 233
diff changeset
239
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
240
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
241
251
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
242 --------------------------------
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
243 ----
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
244 --
254
45b81fcb8a64 equalizer fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 253
diff changeset
245 -- Existence of equalizer satisfies Burroni equations
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
246 --
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
247 ----
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
248
236
e20b81102eee Burroni equational equalizer definition done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
249 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
250 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g )
236
e20b81102eee Burroni equational equalizer definition done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
251 → Burroni A {c} {a} {b} f g e
e20b81102eee Burroni equational equalizer definition done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
252 lemma-equ1 {a} {b} {c} f g e eqa = record {
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
253 α = λ {a} {b} {c} f g e → equalizer1 (eqa {a} {b} {c} f g {e} ) ; -- Hom A c a
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
254 γ = λ {a} {b} {c} {d} f g h → k (eqa {a} {b} {c} f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] )
242
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 241
diff changeset
255 (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
256 δ = λ {a} {b} {c} e f → k (eqa {a} {b} {c} f f {e} ) {a} (id1 A a) (f1=f1 f); -- Hom A a c
246
80d9ef47566b cong-γ1 done, cong-δ1 remains
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 245
diff changeset
257 cong-α = λ {a b c e f g g'} eq → cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq ;
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
258 cong-γ = λ {a} {_} {c} {d} {f} {g} {h} {h'} eq → cong-γ1 {a} {c} {d} {f} {g} {h} {h'} eq ;
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
259 cong-δ = λ {a b c e f f'} f=f' → cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' ;
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
260 b1 = fe=ge (eqa {a} {b} {c} f g {e}) ;
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
261 b2 = λ {d} {h} → lemma-b2 {d} {h};
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
262 b3 = lemma-b3 ;
440
ff36c500962e fix limit
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 300
diff changeset
263 b4 = lemma-b4
211
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
264 } where
216
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
265 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
266 -- e eqa f g f
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 260
diff changeset
267 -- c ---------→ a ------→b
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
268 -- ^ g
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
269 -- |
216
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
270 -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g))))
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
271 -- |
216
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
272 -- d
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
273 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
274 --
216
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
275 -- e o id1 ≈ e → k e ≈ id
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 215
diff changeset
276
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
277 lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer1 (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ]
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
278 lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
279 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
280 equalizer1 (eqa f f) o k (eqa f f) (id a) (f1=f1 f)
215
637b5f58ed28 equ6...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 214
diff changeset
281 ≈⟨ ek=h (eqa f f ) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
282 id a
211
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
283
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
284 lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
285 A [ A [ f o A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ] ]
214
f8afdb9ed99a b4 remains.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 213
diff changeset
286 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
287 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
288 f o ( h o equalizer1 (eqa (f o h) ( g o h )))
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
289 ≈⟨ assoc ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
290 (f o h) o equalizer1 (eqa (f o h) ( g o h ))
221
ea0407fb8f02 on going ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 220
diff changeset
291 ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
292 (g o h) o equalizer1 (eqa (f o h) ( g o h ))
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
293 ≈↑⟨ assoc ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
294 g o ( h o equalizer1 (eqa (f o h) ( g o h )))
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
295
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
296 cong-α1 : {a b c : Obj A } → { e : Hom A c a }
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
297 → {f g g' : Hom A a b } → A [ g ≈ g' ] → A [ equalizer1 (eqa {a} {b} {c} f g {e} )≈ equalizer1 (eqa {a} {b} {c} f g' {e} ) ]
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
298 cong-α1 {a} {b} {c} {e} {f} {g} {g'} eq = let open ≈-Reasoning (A) in refl-hom
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
299 cong-γ1 : {a c d : Obj A } → {f g : Hom A a b} {h h' : Hom A d a } → A [ h ≈ h' ] → { e : Hom A c a} →
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
300 A [ k (eqa f g {e} ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
301 ≈ k (eqa f g {e} ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ) {id1 A d} )) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' ) ]
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
302 cong-γ1 {a} {c} {d} {f} {g} {h} {h'} h=h' {e} = let open ≈-Reasoning (A) in begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
303 k (eqa f g ) {d} ( A [ h o (equalizer1 ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h )
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
304 ≈⟨ uniqueness (eqa f g) ( begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
305 e o k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
248
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 247
diff changeset
306 ≈⟨ ek=h (eqa f g ) ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
307 h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] )))
248
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 247
diff changeset
308 ≈↑⟨ car h=h' ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
309 h o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] )))
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
310 ∎ )⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
311 k (eqa f g ) {d} ( A [ h' o (equalizer1 ( eqa (A [ f o h' ] ) (A [ g o h' ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h' )
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
312
249
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 248
diff changeset
313 cong-δ1 : {a b c : Obj A} {e : Hom A c a } {f f' : Hom A a b} → A [ f ≈ f' ] → A [ k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) ≈
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 248
diff changeset
314 k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ]
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
315 cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
316 begin
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
317 k (eqa {a} {b} {c} f f {e} ) (id a) (f1=f1 f)
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
318 ≈⟨ uniqueness (eqa f f) ( begin
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
319 e o k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f')
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
320 ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
321 id a
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
322 ∎ )⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
323 k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f')
247
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
324
f6e8d6d04af8 equalizer done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 246
diff changeset
325
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
326 lemma-b2 : {d : Obj A} {h : Hom A d a} → A [
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
327 A [ equalizer1 (eqa f g) o k (eqa f g) (A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ]
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
328 ≈ A [ h o equalizer1 (eqa (A [ f o h ]) (A [ g o h ])) ] ]
226
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 225
diff changeset
329 lemma-b2 {d} {h} = let open ≈-Reasoning (A) in
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
330 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
331 equalizer1 (eqa f g) o k (eqa f g) (h o equalizer1 (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h)
215
637b5f58ed28 equ6...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 214
diff changeset
332 ≈⟨ ek=h (eqa f g) ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
333 h o equalizer1 (eqa (f o h ) ( g o h ))
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
334
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
335
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
336 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
337 A [ k (eqa f g) (A [ A [ equalizer1 (eqa f g) o j ] o
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
338 equalizer1 (eqa (A [ f o A [ equalizer1 (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer1 (eqa f g {e} ) o j ] ])) ])
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
339 (lemma-equ4 {a} {b} {c} f g (A [ equalizer1 (eqa f g) o j ]))
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
340 o k (eqa (A [ f o A [ equalizer1 (eqa f g) o j ] ]) (A [ f o A [ equalizer1 (eqa f g) o j ] ]))
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
341 (id1 A d) (f1=f1 (A [ f o A [ equalizer1 (eqa f g) o j ] ])) ]
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
342 ≈ j ]
230
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 229
diff changeset
343 lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
215
637b5f58ed28 equ6...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 214
diff changeset
344 begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
345 ( k (eqa f g) (( ( equalizer1 (eqa f g) o j ) o equalizer1 (eqa (( f o ( equalizer1 (eqa f g {e}) o j ) )) (( g o ( equalizer1 (eqa f g {e}) o j ) ))) ))
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
346 (lemma-equ4 {a} {b} {c} f g (( equalizer1 (eqa f g) o j ))) o
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
347 k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) ))) )
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
348 ≈⟨ car ((uniqueness (eqa f g) ( begin
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
349 equalizer1 (eqa f g) o j
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
350 ≈↑⟨ idR ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
351 (equalizer1 (eqa f g) o j ) o id d
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
352 ≈⟨⟩ -- here we decide e (fej) (gej)' is id d
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
353 ((equalizer1 (eqa f g) o j) o equalizer1 (eqa (f o equalizer1 (eqa f g {e}) o j) (g o equalizer1 (eqa f g {e}) o j)))
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
354 ∎ ))) ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
355 j o k (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer1 (eqa f g) o j ) )))
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
356 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer1 (eqa f g) o j ) )) (( f o ( equalizer1 (eqa f g) o j ) ))) ( begin
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
357 equalizer1 (eqa (f o equalizer1 (eqa f g {e} ) o j) (f o equalizer1 (eqa f g {e}) o j)) o id d
236
e20b81102eee Burroni equational equalizer definition done.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 235
diff changeset
358 ≈⟨ idR ⟩
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
359 equalizer1 (eqa (f o equalizer1 (eqa f g {e}) o j) (f o equalizer1 (eqa f g {e}) o j))
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
360 ≈⟨⟩ -- here we decide e (fej) (fej)' is id d
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
361 id d
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
362 ∎ ))) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
363 j o id d
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
364 ≈⟨ idR ⟩
222
0bc85361b7d0 iso of equalizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 221
diff changeset
365 j
235
8835015a3e1a passed let;s remove yellow
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
366
211
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
367
251
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
368 --------------------------------
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
369 --
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
370 -- Bourroni equations gives an Equalizer
40947f08bab6 comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 250
diff changeset
371 --
211
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
372
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
373 lemma-equ2 : {a b c : Obj A} (f g : Hom A a b) (e : Hom A c a )
443
f526f4b68565 fix IsEqualizer
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 440
diff changeset
374 → ( bur : Burroni A {c} {a} {b} f g e ) → IsEqualizer A {c} {a} {b} (α bur f g e) f g
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
375 lemma-equ2 {a} {b} {c} f g e bur = record {
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
376 fe=ge = fe=ge1 ;
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
377 k = k1 ;
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
378 ek=h = λ {d} {h} {eq} → ek=h1 {d} {h} {eq} ;
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
379 uniqueness = λ {d} {h} {eq} {k'} ek=h → uniqueness1 {d} {h} {eq} {k'} ek=h
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
380 } where
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
381 k1 : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
382 k1 {d} h fh=gh = β bur {d} {a} {b} f g h
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
383 fe=ge1 : A [ A [ f o (α bur f g e) ] ≈ A [ g o (α bur f g e) ] ]
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
384 fe=ge1 = b1 bur
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
385 ek=h1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ (α bur f g e) o k1 {d} h eq ] ≈ h ]
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
386 ek=h1 {d} {h} {eq} = let open ≈-Reasoning (A) in
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
387 begin
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
388 α bur f g e o k1 h eq
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 238
diff changeset
389 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
390 α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) )
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 238
diff changeset
391 ≈⟨ assoc ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
392 ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id d) (f o h)
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 238
diff changeset
393 ≈⟨ car (b2 bur) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
394 ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h)
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 238
diff changeset
395 ≈↑⟨ assoc ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
396 h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h) )
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
397 ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
398 h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
399 ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
400 h o id d
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
401 ≈⟨ idR ⟩
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
402 h
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
403
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
404 uniqueness1 : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } →
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
405 A [ A [ (α bur f g e) o k' ] ≈ h ] → A [ k1 {d} h eq ≈ k' ]
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
406 uniqueness1 {d} {h} {eq} {k'} ek=h = let open ≈-Reasoning (A) in
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
407 begin
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
408 k1 {d} h eq
239
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 238
diff changeset
409 ≈⟨⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
410 γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h)
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
411 ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
412 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) (f o h)
245
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 244
diff changeset
413 ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 252
diff changeset
414 γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') )
240
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 239
diff changeset
415 ≈⟨ b4 bur ⟩
238
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
416 k'
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
417
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
418
c8db99cdf72a Burrnoi to Equalizer problem written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 237
diff changeset
419
225
1a9f20917fbd comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 224
diff changeset
420 -- end
212
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
421
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
422
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 211
diff changeset
423
215
637b5f58ed28 equ6...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 214
diff changeset
424
637b5f58ed28 equ6...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 214
diff changeset
425