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

comparison src/zorn.agda @ 1096:55ab5de1ae02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovery
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2022 12:54:05 +0900
parents 63c1167b2343
children 40345abc0949
comparison
equal deleted inserted replaced
1095:08b6aa6870d9 1096:55ab5de1ae02
2 open import Level hiding ( suc ; zero ) 2 open import Level hiding ( suc ; zero )
3 open import Ordinals 3 open import Ordinals
4 open import Relation.Binary 4 open import Relation.Binary
5 open import Relation.Binary.Core 5 open import Relation.Binary.Core
6 open import Relation.Binary.PropositionalEquality 6 open import Relation.Binary.PropositionalEquality
7 import OD hiding ( _⊆_ ) 7 import OD
8 module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where 8 module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where
9 9
10 -- 10 --
11 -- Zorn-lemma : { A : HOD } 11 -- Zorn-lemma : { A : HOD }
12 -- → o∅ o< & A 12 -- → o∅ o< & A
215 215
216 -- open import Relation.Binary.Properties.Poset as Poset 216 -- open import Relation.Binary.Properties.Poset as Poset
217 217
218 IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n) 218 IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n)
219 IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b) → Tri (a < b) (a ≡ b) (b < a ) 219 IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b) → Tri (a < b) (a ≡ b) (b < a )
220
221 _⊆_ : ( A B : HOD ) → Set n
222 _⊆_ A B = {x : Ordinal } → odef A x → odef B x
223 220
224 ⊆-IsTotalOrderSet : { A B : HOD } → B ⊆ A → IsTotalOrderSet A → IsTotalOrderSet B 221 ⊆-IsTotalOrderSet : { A B : HOD } → B ⊆ A → IsTotalOrderSet A → IsTotalOrderSet B
225 ⊆-IsTotalOrderSet {A} {B} B⊆A T ax ay = T (B⊆A ax) (B⊆A ay) 222 ⊆-IsTotalOrderSet {A} {B} B⊆A T ax ay = T (B⊆A ax) (B⊆A ay)
226 223
227 record HasPrev (A B : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal ) : Set n where 224 record HasPrev (A B : HOD) ( f : Ordinal → Ordinal ) (x : Ordinal ) : Set n where