# HG changeset patch # User Shinji KONO # Date 1593335344 -32400 # Node ID 304c271b3d47d67290241766e7c6f6b4e2c9350d # Parent b012a915bbb5a14c904ef34ed19742276689c4c6 HOD and reduction mapping of Ordinals diff -r b012a915bbb5 -r 304c271b3d47 OD.agda --- a/OD.agda Wed Jun 24 14:05:38 2020 +0900 +++ b/OD.agda Sun Jun 28 18:09:04 2020 +0900 @@ -67,6 +67,24 @@ -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, -- we need explict assumption on sup. +record HOD (odmax : Ordinal) : Set (suc n) where + field + hmax : {x : Ordinal } → x o< odmax + hdef : Ordinal → Set n + +record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where + field + os→ : (x : Ordinal) → x o< maxordinal → Ordinal + os← : Ordinal → Ordinal + os←limit : (x : Ordinal) → os← x o< maxordinal + os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x + os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x + +open HOD + +-- HOD→OD : {x : Ordinal} → HOD x → OD +-- HOD→OD hod = record { def = hdef {!!} } + record ODAxiom : Set (suc n) where -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) field @@ -83,6 +101,25 @@ -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) +record HODAxiom : Set (suc n) where + -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) + field + mod : Ordinal + mod-limit : ¬ ((y : Ordinal) → mod ≡ osuc y) + os : OrdinalSubset mod + od→ord : HOD mod → Ordinal + ord→od : Ordinal → HOD mod + c<→o< : {x y : HOD mod } → hdef y (od→ord x) → od→ord x o< od→ord y + oiso : {x : HOD mod } → ord→od ( od→ord x ) ≡ x + diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x + ==→o≡ : { x y : OD } → (x == y) → x ≡ y + -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) + sup-o : ( HOD mod → Ordinal ) → Ordinal + sup-o< : { ψ : HOD mod → Ordinal } → ∀ {x : HOD mod } → ψ x o< sup-o ψ + -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use + -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal + -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) + postulate odAxiom : ODAxiom open ODAxiom odAxiom diff -r b012a915bbb5 -r 304c271b3d47 Ordinals.agda --- a/Ordinals.agda Wed Jun 24 14:05:38 2020 +0900 +++ b/Ordinals.agda Sun Jun 28 18:09:04 2020 +0900 @@ -20,6 +20,7 @@ ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) + is-limit : { x : ord } → Dec ( ¬ ((y : ord) → x ≡ osuc y) ) TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x