Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/OPair.agda @ 1164:5e065f0a7ba2

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 Sat, 21 Jan 2023 09:12:10 +0900
parents adba530ce1f0
children 46dc298bdd77
comparison
equal deleted inserted replaced
1163:cd54ee498249 1164:5e065f0a7ba2
252 ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 252 ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) ))
253 253
254 ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B → HOD 254 ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B → HOD
255 ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 255 ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) ))
256 256
257 record PProj1 (L : HOD) (x : Ordinal) : Set n where 257 -- simple version
258
259 record ZProj1 (L : HOD) (x : Ordinal) : Set n where
258 field 260 field
259 pq : Ordinal 261 pq : Ordinal
260 opq : ord-pair pq 262 opq : ord-pair pq
261 Lpq : odef L pq 263 Lpq : odef L pq
262 x=pi1 : x ≡ pi1 opq 264 x=pi1 : x ≡ pi1 opq
263 265
264 -- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px ) ))) 266 -- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px ) )))
265 267
266 Proj1PP : (L P Q : HOD) → HOD 268 Proj1 : (L P Q : HOD) → HOD
267 Proj1PP L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → PProj1 L y) } ; odmax = & P ; <odmax = odef∧< } 269 Proj1 L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → ZProj1 L y) } ; odmax = & P ; <odmax = odef∧< }
268 270
269 record PProj2 (L : HOD) (x : Ordinal) : Set n where 271 record ZProj2 (L : HOD) (x : Ordinal) : Set n where
270 field 272 field
271 pq : Ordinal 273 pq : Ordinal
272 opq : ord-pair pq 274 opq : ord-pair pq
273 Lpq : odef L pq 275 Lpq : odef L pq
274 x=pi2 : x ≡ pi2 opq 276 x=pi2 : x ≡ pi2 opq
275 277
276 Proj2PP : (L P Q : HOD) → HOD 278 Proj2 : (L P Q : HOD) → HOD
277 Proj2PP L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → PProj2 L y) } ; odmax = & Q ; <odmax = odef∧< } 279 Proj2 L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → ZProj2 L y) } ; odmax = & Q ; <odmax = odef∧< }
278 280