# HG changeset patch # User Shinji KONO # Date 1593482902 -32400 # Node ID bf01e924e62e7f0c2d5a2f6d5cd993940a1a00a5 # Parent 73a2a8ec9603b855edf89cac181c6151427223d3 ... diff -r 73a2a8ec9603 -r bf01e924e62e OD.agda --- a/OD.agda Tue Jun 30 08:55:12 2020 +0900 +++ b/OD.agda Tue Jun 30 11:08:22 2020 +0900 @@ -222,9 +222,6 @@ OPwr : (A : HOD ) → HOD OPwr A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) ) --- _⊆_ : ( A B : HOD ) → ∀{ x : HOD } → Set n --- _⊆_ A B {x} = A ∋ x → B ∋ x - record _⊆_ ( A B : HOD ) : Set (suc n) where field incl : { x : HOD } → A ∋ x → B ∋ x @@ -250,9 +247,6 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy --- minimal-2 : (x : HOD ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) --- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} ) - HOD→ZF : ZF HOD→ZF = record { ZFSet = HOD @@ -271,7 +265,7 @@ Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ;