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 }