# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# 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