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

comparison OD.agda @ 381:d2cb5278e46d

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 Tue, 21 Jul 2020 14:34:27 +0900
parents 853ead1b56b8
children 8b0715e28b33
comparison
equal deleted inserted replaced
380:0a116938a564 381:d2cb5278e46d
74 -- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, 74 -- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
75 -- we need explict assumption on sup. 75 -- we need explict assumption on sup.
76 -- 76 --
77 -- ==→o≡ is necessary to prove axiom of extensionality. 77 -- ==→o≡ is necessary to prove axiom of extensionality.
78 78
79 data One : Set n where 79 data One {n : Level } : Set n where
80 OneObj : One 80 OneObj : One
81 81
82 -- Ordinals in OD , the maximum 82 -- Ordinals in OD , the maximum
83 Ords : OD 83 Ords : OD
84 Ords = record { def = λ x → One } 84 Ords = record { def = λ x → One }