# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564909740 -32400
# Node ID 5b9b6ef971dd5f56903388536f505b78f0f0b268
# Parent  f15eaa7c5932e76201879b4957603d914efc99de
Cardinal start

diff -r f15eaa7c5932 -r 5b9b6ef971dd OD.agda
--- a/OD.agda	Fri Aug 02 21:31:45 2019 +0900
+++ b/OD.agda	Sun Aug 04 18:09:00 2019 +0900
@@ -260,7 +260,6 @@
     ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
    } 
 
-
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
 -- L (Φ 0) = Φ
@@ -624,3 +623,34 @@
                      ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                    }
 
+         ------------
+         --
+         -- Onto map
+         --          def X x ->  xmap
+         --     X ---------------------------> Y
+         --          ymap   <-  def Y y
+         --
+         record Onto {n : Level } (X Y : OD {suc n})  : Set (suc (suc n)) where
+            field
+                xmap : (x : Ordinal {suc n}) → Ordinal {suc n} 
+                ymap : (y : Ordinal {suc n}) → Ordinal {suc n} 
+                xmap-on-Y  : (x :  Ordinal {suc n} ) → def X x  → def Y (xmap x)  
+                ymap-on-X  : (y :  Ordinal {suc n} ) → def Y y  → def X (ymap y)  
+                onto-iso : (y :  Ordinal {suc n} ) → def Y y → xmap ( ymap y ) ≡ y
+
+         record Cardinal {n : Level } (X  : OD {suc n}) : Set (suc (suc n)) where
+            field
+                cardinal : Ordinal {suc n}
+                conto : Onto (Ord cardinal) X 
+                cmax : ( y : Ordinal {suc n} ) → cardinal o< y → ¬ Onto (Ord y) X 
+
+         cardinal : {n : Level } (X  : OD {suc n}) → Cardinal X
+         cardinal {n} X = record {
+                cardinal = sup-o ( λ x → cardinal-p x )
+              ; conto = {!!}
+              ; cmax = {!!}
+            } where
+             cardinal-p : (x  : Ordinal {suc n}) →  Ordinal {suc n}
+             cardinal-p x with p∨¬p ( Onto (Ord x) X ) 
+             cardinal-p x | case1 True = x
+             cardinal-p x | case2 False = o∅