### changeset 421:cb067605fea0

...
author Shinji KONO Fri, 31 Jul 2020 17:54:52 +0900 53422a8ea836 44a484f17f26 cardinal.agda 1 files changed, 12 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
```--- 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 }```