# HG changeset patch # User Shinji KONO # Date 1594551337 -32400 # Node ID feb0fcc430a95db87597747567fd8e23fc6318a7 # Parent bca043423554111f193dfded0a6c9ff1cef460d4 ... diff -r bca043423554 -r feb0fcc430a9 OD.agda --- a/OD.agda Sun Jul 12 12:32:42 2020 +0900 +++ b/OD.agda Sun Jul 12 19:55:37 2020 +0900 @@ -103,12 +103,13 @@ sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ --- another form of infinite --- pair-ord< : {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x) - postulate odAxiom : ODAxiom open ODAxiom odAxiom +-- possible restriction +hod-ord< : {x : HOD } → Set n +hod-ord< {x} = od→ord x o< next (odmax x) + -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) @@ -221,6 +222,9 @@ lemma {t} (case1 refl) = omax-x _ _ lemma {t} (case2 refl) = omax-y _ _ +-- another form of infinite +pair-ord< : {x : Ordinal } → Set n +pair-ord< {x} = od→ord ( ord→od x , ord→od x ) o< next x -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) @@ -370,15 +374,23 @@ infinite : HOD infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x