diff Ordinals.agda @ 302:304c271b3d47

HOD and reduction mapping of Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jun 2020 18:09:04 +0900
parents 63df67b6281c
children b172ab9f12bc
line wrap: on
line diff
--- 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