Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 1096:55ab5de1ae02
recovery
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 23 Dec 2022 12:54:05 +0900 |
| parents | 63c1167b2343 |
| children | 40345abc0949 |
line wrap: on
line diff
--- a/src/zorn.agda Thu Dec 22 15:10:31 2022 +0900 +++ b/src/zorn.agda Fri Dec 23 12:54:05 2022 +0900 @@ -4,7 +4,7 @@ open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality -import OD hiding ( _⊆_ ) +import OD module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where -- @@ -218,9 +218,6 @@ IsTotalOrderSet : ( A : HOD ) → Set (Level.suc n) IsTotalOrderSet A = {a b : HOD} → odef A (& a) → odef A (& b) → Tri (a < b) (a ≡ b) (b < a ) -_⊆_ : ( A B : HOD ) → Set n -_⊆_ A B = {x : Ordinal } → odef A x → odef B x - ⊆-IsTotalOrderSet : { A B : HOD } → B ⊆ A → IsTotalOrderSet A → IsTotalOrderSet B ⊆-IsTotalOrderSet {A} {B} B⊆A T ax ay = T (B⊆A ax) (B⊆A ay)