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

comparison OD.agda @ 301:b012a915bbb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
contradiction found ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jun 2020 14:05:38 +0900
parents e70980bd80c7
children 304c271b3d47
comparison
equal deleted inserted replaced
300:e70980bd80c7 301:b012a915bbb5
93 Ords : OD 93 Ords : OD
94 Ords = record { def = λ x → One } 94 Ords = record { def = λ x → One }
95 95
96 maxod : {x : OD} → od→ord x o< od→ord Ords 96 maxod : {x : OD} → od→ord x o< od→ord Ords
97 maxod {x} = c<→o< OneObj 97 maxod {x} = c<→o< OneObj
98
99 -- we have to avoid this contradiction
100
101 bad-bad : ⊥
102 bad-bad = osuc-< <-osuc (c<→o< { record { def = λ x → One }} OneObj)
98 103
99 -- Ordinal in OD ( and ZFSet ) Transitive Set 104 -- Ordinal in OD ( and ZFSet ) Transitive Set
100 Ord : ( a : Ordinal ) → OD 105 Ord : ( a : Ordinal ) → OD
101 Ord a = record { def = λ y → y o< a } 106 Ord a = record { def = λ y → y o< a }
102 107