Mercurial > hg > Members > kono > Proof > category

comparison CCChom.agda @ 787:ca5eba647990

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Apr 2019 20:07:22 +0900
parents 287d25c87b60
children a3e124e36acf
comparison
equal deleted inserted replaced
786:287d25c87b60 787:ca5eba647990
41 field 41 field
42 ≅→ : Hom A a b → Hom B a' b' 42 ≅→ : Hom A a b → Hom B a' b'
43 ≅← : Hom B a' b' → Hom A a b 43 ≅← : Hom B a' b' → Hom A a b
44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] 44 iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ]
45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] 45 iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ]
46 cong→ : {f g : Hom A a b } → A [ f ≈ g ] → B [ ≅→ f ≈ ≅→ g ]
47 cong← : {f g : Hom B a' b'} → B [ f ≈ g ] → A [ ≅← f ≈ ≅← g ]
46 48
47 49
48 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) 50 record IsCCChom {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A)
49 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where 51 ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
50 field 52 field
71 CCC→hom A c = record { 73 CCC→hom A c = record {
72 one = CCC.１ c 74 one = CCC.１ c
73 ; _*_ = CCC._∧_ c 75 ; _*_ = CCC._∧_ c
74 ; _^_ = CCC._<=_ c 76 ; _^_ = CCC._<=_ c
75 ; isCCChom = record { 77 ; isCCChom = record {
76 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 } 78 ccc-1 = λ {a} {b} {c'} → record { ≅→ = c101 ; ≅← = c102 ; iso→ = c103 {a} {b} {c'} ; iso← = c104 ; cong← = c105 ; cong→ = c106 }
77 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 } 79 ; ccc-2 = record { ≅→ = c201 ; ≅← = c202 ; iso→ = c203 ; iso← = c204 ; cong← = c205; cong→ = c206 }
78 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 } 80 ; ccc-3 = record { ≅→ = c301 ; ≅← = c302 ; iso→ = c303 ; iso← = c304 ; cong← = c305 ; cong→ = c306 }
79 } 81 }
80 } where 82 } where
81 c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj 83 c101 : {a : Obj A} → Hom A a (CCC.１ c) → Hom OneCat OneObj OneObj
82 c101 _ = OneObj 84 c101 _ = OneObj
83 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c) 85 c102 : {a : Obj A} → Hom OneCat OneObj OneObj → Hom A a (CCC.１ c)
100 c302 f = CCC._* c f 102 c302 f = CCC._* c f
101 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ] 103 c303 : { c₁ a b : Obj A} → {f : Hom A ((c CCC.∧ a) b) c₁} → A [ (c301 ( c302 f )) ≈ f ]
102 c303 = IsCCC.e4a (CCC.isCCC c) 104 c303 = IsCCC.e4a (CCC.isCCC c)
103 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ] 105 c304 : { c₁ a b : Obj A} → {f : Hom A a ((c CCC.<= c₁) b)} → A [ (c302 ( c301 f )) ≈ f ]
104 c304 = IsCCC.e4b (CCC.isCCC c) 106 c304 = IsCCC.e4b (CCC.isCCC c)
107 c105 : {a : Obj A } {f g : Hom OneCat OneObj OneObj} → _[_≈_] OneCat {OneObj} {OneObj} f g → A [ c102 {a} f ≈ c102 {a} g ]
108 c105 refl = let open ≈-Reasoning A in refl-hom
109 c106 : { a : Obj A } {f g : Hom A a (CCC.１ c)} → A [ f ≈ g ] → _[_≈_] OneCat {OneObj} {OneObj} OneObj OneObj
110 c106 _ = refl
111 c205 : { a b c₁ : Obj A } {f g : Hom (A × A) (c₁ , c₁) (a , b)} → (A × A) [ f ≈ g ] → A [ c202 f ≈ c202 g ]
112 c205 f=g = IsCCC.π-cong (CCC.isCCC c ) (proj₁ f=g ) (proj₂ f=g )
113 c206 : { a b c₁ : Obj A } {f g : Hom A c₁ ((c CCC.∧ a) b)} → A [ f ≈ g ] → (A × A) [ c201 f ≈ c201 g ]
114 c206 {a} {b} {c₁} {f} {g} f=g = ( begin
115 CCC.π c o f
116 ≈⟨ cdr f=g ⟩
117 CCC.π c o g
118 ∎ ) , ( begin
119 CCC.π' c o f
120 ≈⟨ cdr f=g ⟩
121 CCC.π' c o g
122 ∎ ) where open ≈-Reasoning A
123 c305 : { a b c₁ : Obj A } {f g : Hom A ((c CCC.∧ a) b) c₁} → A [ f ≈ g ] → A [ (c CCC.*) f ≈ (c CCC.*) g ]
124 c305 f=g = IsCCC.*-cong (CCC.isCCC c ) f=g
125 c306 : { a b c₁ : Obj A } {f g : Hom A a ((c CCC.<= c₁) b)} → A [ f ≈ g ] → A [ c301 f ≈ c301 g ]
126 c306 {a} {b} {c₁} {f} {g} f=g = begin
127 CCC.ε c o CCC.<_,_> c ( f o CCC.π c ) ( CCC.π' c )
128 ≈⟨ cdr ( IsCCC.π-cong (CCC.isCCC c ) (car f=g ) refl-hom) ⟩
129 CCC.ε c o CCC.<_,_> c ( g o CCC.π c ) ( CCC.π' c )
130 ∎ where open ≈-Reasoning A
131
105 132
106 open CCChom 133 open CCChom
107 open IsCCChom 134 open IsCCChom
108 open IsoS 135 open IsoS
109 136
145 ; e3b = e3b 172 ; e3b = e3b
146 ; e3c = e3c 173 ; e3c = e3c
147 ; π-cong = π-cong 174 ; π-cong = π-cong
148 ; e4a = e4a 175 ; e4a = e4a
149 ; e4b = e4b 176 ; e4b = e4b
177 ; *-cong = *-cong
150 } where 178 } where
151 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj 179 e20 : ∀ ( f : Hom OneCat OneObj OneObj ) → _[_≈_] OneCat {OneObj} {OneObj} f OneObj
152 e20 OneObj = refl 180 e20 OneObj = refl
153 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ] 181 e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ]
154 e2 {a} f = begin 182 e2 {a} f = begin
159 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩ 187 λ y → ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) y ) (e20 ( ≅→ ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) f) ) ⟩
160 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj 188 ≅← ( ccc-1 (isCCChom h ) {a} {OneObj} {OneObj} ) OneObj
161 ≈⟨⟩ 189 ≈⟨⟩
162 ○ a 190 ○ a
163 ∎ where open ≈-Reasoning A 191 ∎ where open ≈-Reasoning A
164 e30 : {a b c d e : Obj A} → { f : Hom A ((_*_ h b) c) ((_*_ h d) e) } → {g : Hom A a ((_*_ h b) c) } 192 --
165 → A [ A [ proj₁ (≅→ (ccc-2 (isCCChom h)) f ) o g ] ≈ proj₁ (≅→ (ccc-2 (isCCChom h)) (A [ f o g ] ) ) ] 193 -- g id
166 e30 = {!!} 194 -- a -------------> b * c ------> b * c
167 e31 : {a b c d e : Obj A} → {i : Hom (A × A) (b , c) (d , e )} → { f : Hom A a b } → {g : Hom A a c } 195 --
168 → A [ A [ {!!} o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ] ≈ ( ≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A) i (f , g ) )) ] 196 -- a -------------> b * c ------> b
197 -- a -------------> b * c ------> c
198 --
199 e31 : {a b c : Obj A} → {f : Hom A ((_*_ h b) c) ((_*_ h b) c) } → {g : Hom A a ((_*_ h b) c) }
200 → (A × A) [ (A × A) [ ≅→ (ccc-2 (isCCChom h)) f o (g , g ) ] ≈ ≅→ (ccc-2 (isCCChom h)) ( A [ f o g ] ) ]
169 e31 = {!!} 201 e31 = {!!}
202 e30 : {a b c : Obj A} → {g : Hom A a ((_*_ h b) c) }
203 → (A × A) [ (A × A) [ (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g) ] ≈ (≅→ (ccc-2 (isCCChom h)) (A [ id1 A ((_*_ h b) c) o g ] ) ) ]
204 e30 {a} {b} {c} {g} = begin
205 (≅→ (ccc-2 (isCCChom h)) (id1 A ((_*_ h b) c))) o (g , g)
206 ≈⟨⟩
207 ( π , π' ) o ( g , g )
208 ≈⟨⟩
209 ( _[_o_] A π g , _[_o_] A π' g )
210 ≈↑⟨ cdr1 A (iso← (ccc-2 (isCCChom h))) , cdr1 A (iso← (ccc-2 (isCCChom h))) ⟩
211 ( _[_o_] A (proj₁ ( ≅→ ( ccc-2 (isCCChom h ) ) (id1 A (_*_ h b c) ))) (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h))) g)) ,
212 _[_o_] A π' (≅← (ccc-2 (isCCChom h))((≅→ (ccc-2 (isCCChom h))) g)) )
213 ≈⟨ {!!} ⟩
214 ( proj₁ ((≅→ (ccc-2 (isCCChom h))) g) , proj₂ ((≅→ (ccc-2 (isCCChom h))) g) )
215 ≈⟨⟩
216 ≅→ (ccc-2 (isCCChom h)) g
217 ≈↑⟨ cong→ (ccc-2 (isCCChom h)) ( idL1 A ) ⟩
218 ≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ((_*_ h b) c)) g )
219 ∎ where open ≈-Reasoning (A × A)
220 cong-proj₁ : {a b c d : Obj A} → { f g : Hom (A × A) ( a , b ) ( c , d ) } → (A × A) [ f ≈ g ] → A [ proj₁ f ≈ proj₁ g ]
221 cong-proj₁ eq = proj₁ eq
170 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ] 222 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o <,> f g ] ≈ f ]
171 e3a {a} {b} {c} {f} {g} = begin 223 e3a {a} {b} {c} {f} {g} = begin
172 π o <,> f g 224 π o <,> f g
173 ≈⟨⟩ 225 ≈⟨⟩
174 proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g)) 226 proj₁ (≅→ (ccc-2 (isCCChom h)) (id1 A (_*_ h a b) )) o (≅← (ccc-2 (isCCChom h)) (f , g))
175 ≈⟨ e30 ⟩ 227 ≈⟨ cong-proj₁ e30 ⟩
176 proj₁ (≅→ (ccc-2 (isCCChom h)) (_[_o_] A ( id1 A ( _*_ h a b )) ( ≅← (ccc-2 (isCCChom h)) (f , g) ) )) 228 proj₁ (≅→ (ccc-2 (isCCChom h)) (( id1 A ( _*_ h a b )) o ( ≅← (ccc-2 (isCCChom h)) (f , g) ) ))
177 ≈⟨ {!!} ⟩ 229 ≈⟨ cong-proj₁ ( cong→ (ccc-2 (isCCChom h)) idL ) ⟩
178 proj₁ (≅→ (ccc-2 (isCCChom h)) (≅← (ccc-2 (isCCChom h)) ( _[_o_] (A × A ) ( id1 A a , id1 A b ) (f , g) ))) 230 proj₁ (≅→ (ccc-2 (isCCChom h)) ( ≅← (ccc-2 (isCCChom h)) (f , g) ))
179 ≈⟨ {!!} ⟩ 231 ≈⟨ cong-proj₁ ( iso→ (ccc-2 (isCCChom h))) ⟩
180 proj₁ ( f , g ) 232 proj₁ ( f , g )
181 ≈⟨⟩ 233 ≈⟨⟩
182 f 234 f
183 ∎ where open ≈-Reasoning A 235 ∎ where open ≈-Reasoning A
184 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ] 236 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o <,> f g ] ≈ g ]
188 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ] 240 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ <,> f g ≈ <,> f' g' ]
189 π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin 241 π-cong {a} {b} {c} {f} {f'} {g} {g'} eq1 eq2 = begin
190 <,> f g 242 <,> f g
191 ≈⟨⟩ 243 ≈⟨⟩
192 ≅← (ccc-2 (isCCChom h)) (f , g) 244 ≅← (ccc-2 (isCCChom h)) (f , g)
193 ≈⟨ ≡-cong {!!} {!!} ⟩ 245 ≈⟨ cong← (ccc-2 (isCCChom h)) ( eq1 , eq2 ) ⟩
194 ≅← (ccc-2 (isCCChom h)) (f' , g') 246 ≅← (ccc-2 (isCCChom h)) (f' , g')
195 ≈⟨⟩ 247 ≈⟨⟩
196 <,> f' g' 248 <,> f' g'
197 ∎ where open ≈-Reasoning A 249 ∎ where open ≈-Reasoning A
250 e40 : {a c : Obj A} → { f : Hom A (_*_ h a c ) a } → A [ ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) f) ≈ f ]
251 e40 = iso→ (ccc-3 (isCCChom h))
252 e41 : {a c : Obj A} → { f : Hom A a (_^_ h c a )} → A [ ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) f) ≈ f ]
253 e41 = iso← (ccc-3 (isCCChom h))
198 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ] 254 e4a : {a b c : Obj A} → { k : Hom A (c /\ b) a } → A [ A [ ε o ( <,> ( A [ (k *) o π ] ) π') ] ≈ k ]
199 e4a {a} {b} {c} {k} = begin 255 e4a {a} {b} {c} {k} = begin
200 ε o ( <,> ((k *) o π ) π' ) 256 ε o ( <,> ((k *) o π ) π' )
201 ≈⟨⟩ 257 ≈⟨⟩
202 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o 258 ≅→ (ccc-3 (isCCChom h)) (id1 A (_^_ h a b)) o (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
203 (≅← (ccc-2 (isCCChom h)) ((( ≅← (ccc-3 (isCCChom h)) k) o π ) , π'))
204 ≈⟨ {!!} ⟩ 259 ≈⟨ {!!} ⟩
260 ≅→ (ccc-3 (isCCChom h)) (≅← (ccc-3 (isCCChom h)) k)
261 ≈⟨ iso→ (ccc-3 (isCCChom h)) ⟩
205 k 262 k
206 ∎ where open ≈-Reasoning A 263 ∎ where open ≈-Reasoning A
207 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ] 264 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o ( <,> ( A [ k o π ] ) π' ) ] ) * ≈ k ]
208 e4b = {!!} 265 e4b {a} {b} {c} {k} = begin
209 266 ( ε o ( <,> ( k o π ) π' ) ) *
267 ≈⟨⟩
268 ≅← (ccc-3 (isCCChom h)) ( ≅→ ( ccc-3 (isCCChom h ) {_^_ h a b} {b} ) (id1 A ( _^_ h a b )) o (≅← (ccc-2 (isCCChom h)) ( k o π , π')))
269 ≈⟨ {!!} ⟩
270 ≅← (ccc-3 (isCCChom h)) (≅→ (ccc-3 (isCCChom h)) k)
271 ≈⟨ iso← (ccc-3 (isCCChom h)) ⟩
272 k
273 ∎ where open ≈-Reasoning A
274 *-cong : {a b c : Obj A} {f f' : Hom A (a /\ b) c} → A [ f ≈ f' ] → A [ f * ≈ f' * ]
275 *-cong eq = cong← ( ccc-3 (isCCChom h )) eq
276
277
278