Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff Ordinals.agda @ 309:d4802179a66f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jun 2020 00:17:05 +0900
parents b172ab9f12bc
children 21203fe0342f
line wrap: on
line diff
--- a/Ordinals.agda	Tue Jun 30 00:05:16 2020 +0900
+++ b/Ordinals.agda	Tue Jun 30 00:17:05 2020 +0900
@@ -200,3 +200,11 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        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
+