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

comparison OD.agda @ 299:171f23379e2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
better to use ordinal number hierachy to create HOD
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jun 2020 14:45:55 +0900
parents 3795ffb127d0
children
comparison
equal deleted inserted replaced
298:3795ffb127d0 299:171f23379e2e
96 96
97 -- Ordinals in OD , the maximum 97 -- Ordinals in OD , the maximum
98 Ords : OD 98 Ords : OD
99 Ords = record { def = λ x → One } 99 Ords = record { def = λ x → One }
100 100
101 -- maxod : {x : OD} → od→ord x o< od→ord Ords 101 maxod0 : {x : OD} → od→ord x o< od→ord Ords
102 -- maxod {x} = c<→o< OneObj 102 maxod0 {x} = c<→o< OneObj
103 103
104 -- Ordinal in OD ( and ZFSet ) Transitive Set 104 -- Ordinal in OD ( and ZFSet ) Transitive Set
105 Ord : ( a : Ordinal ) → OD 105 Ord : ( a : Ordinal ) → OD
106 Ord a = record { def = λ y → y o< a } 106 Ord a = record { def = λ y → y o< a }
107 107