# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596092796 -32400
# Node ID aa306f5dab9b0f3b7624d3ea8c8f536fe8ac5a4a
# Parent  b00d58b3dc579ee756d0957fef6c7f48e5c9a563
add VL

diff -r b00d58b3dc57 -r aa306f5dab9b Ordinals.agda
--- a/Ordinals.agda	Thu Jul 30 08:15:56 2020 +0900
+++ b/Ordinals.agda	Thu Jul 30 16:06:36 2020 +0900
@@ -13,6 +13,11 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
+record Oprev {n : Level} (ord : Set n) (osuc :  ord → ord ) (x : ord ) : Set (suc n) where
+   field
+     oprev : ord
+     oprev=x : osuc oprev ≡ x 
+
 record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
      Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
@@ -20,7 +25,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)  
-     not-limit-p :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
+     Oprev-p :  ( x : ord  ) → Dec ( Oprev ord osuc x )
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -66,6 +71,7 @@
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
         TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
+        Oprev-p = IsOrdinals.Oprev-p  (Ordinals.isOrdinal O)
 
         x<nx = IsNext.x<nx (Ordinals.isNext O)
         osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
diff -r b00d58b3dc57 -r aa306f5dab9b VL.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/VL.agda	Thu Jul 30 16:06:36 2020 +0900
@@ -0,0 +1,43 @@
+open import Level
+open import Ordinals
+module VL {n : Level } (O : Ordinals {n}) where
+
+open import zf
+open import logic
+import OD 
+open import Relation.Nullary 
+open import Relation.Binary 
+open import Data.Empty 
+open import Relation.Binary
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+import BAlgbra 
+open BAlgbra O
+open inOrdinal O
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+-- import ODC
+open _∧_
+open _∨_
+open Bool
+open HOD
+
+-- The cumulative hierarchy 
+--    V 0 := ∅ .
+--    V β + 1 := P ( V β ) .
+--    V λ := ⋃ β < λ V β .
+
+{-# TERMINATING #-}
+V : ( β : Ordinal ) → HOD
+V β = TransFinite1  Vβ₁ β where
+   Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
+   Vβ₁ x Vβ₀ with trio< x o∅
+   Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
+   Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = od∅ 
+   Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p  x
+   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
+   Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = Vβ<α x where
+      Vβ<α : (α : Ordinal ) → HOD 
+      Vβ<α α = record { od = record { def = λ x → (x o< α ) ∧ odef (V x) x  } ; odmax = α; <odmax = λ {x} lt → proj1 lt }