--- a/cardinal.agda	Fri Jul 31 17:42:25 2020 +0900
+++ b/cardinal.agda	Fri Jul 31 17:54:52 2020 +0900
@@ -48,20 +48,16 @@
     → odef (FuncP A B) (od→ord  (Replace A (λ x → < x , f x > )))
 FuncP∋f = {!!}
 
-Func→f : {A B f x : HOD} → def Func (od→ord f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
-Func→f = {!!}
-
-Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}  
-Func₁ = {!!}
-
-Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
-Cod = {!!}
-
-1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
-1-1 = {!!}
-
-onto : {A B f : HOD} → def Func (od→ord f) → {!!}
-onto  = {!!}
+-- Func→f : {A B f x : HOD} → def Func (od→ord f)  → (x : HOD ) → A ∋ x  → ( HOD ∧ ((y : HOD ) → B ∋ y ))
+-- Func→f = {!!}
+-- Func₁ : {A B f : HOD} → def Func (od→ord f) → {!!}  
+-- Func₁ = {!!}
+-- Cod : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- Cod = {!!}
+-- 1-1 : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- 1-1 = {!!}
+-- onto : {A B f : HOD} → def Func (od→ord f) → {!!}
+-- onto  = {!!}
 
 record Bijection (A B : Ordinal ) : Set n where
    field
@@ -69,8 +65,8 @@
        fun← : Ordinal → Ordinal
        fun→inA : (x : Ordinal) → odef (ord→od A) ( fun→ x )
        fun←inB : (x : Ordinal) → odef (ord→od B) ( fun← x )
-       fiso→ : (x : Ordinal ) → odef (ord→od A)  x → fun→ ( fun← x ) ≡ x
-       fiso← : (x : Ordinal ) → odef (ord→od B)  x → fun← ( fun→ x ) ≡ x
+       fiso→ : (x : Ordinal ) → odef (ord→od B)  x → fun→ ( fun← x ) ≡ x
+       fiso← : (x : Ordinal ) → odef (ord→od A)  x → fun← ( fun→ x ) ≡ x
        
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }