Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 299:171f23379e2e
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 |