--- a/src/VL.agda	Fri Jun 28 17:41:43 2024 +0900
+++ b/src/VL.agda	Fri Jun 28 20:55:38 2024 +0900
@@ -1,35 +1,51 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
+
 open import Level
 open import Ordinals
-module VL {n : Level } (O : Ordinals {n}) where
+import HODBase
+import OD
+open import Relation.Nullary
+module VL {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom ) where
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 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 BAlgebra 
-open BAlgebra O
-open inOrdinal O
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
---  open Ordinals.IsNext isNext
+open import nat
+
 open OrdUtil O
-open ODUtil O
+open ODUtil O HODAxiom  ho<
 
-open OD O
-open OD.OD
-open ODAxiom odAxiom
--- import ODC
 open _∧_
 open _∨_
 open Bool
-open HOD
+
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+
+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⊔_ )
+
 
 -- The cumulative hierarchy 
 --    V 0 := ∅ 
@@ -59,15 +75,15 @@
      β  : Ordinal
      ov : odef (TransFinite  V1 β) x 
 
-Vn∅ : Vn
-Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
+-- Vn∅ : Vn
+-- Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
 
-vsuc : Vn → Vn
-vsuc v = ?
+-- vsuc : Vn → Vn
+-- vsuc v = ?
 
-v< : Vn → Vn → Set n
-v< x y = ?
+-- v< : Vn → Vn → Set n
+-- v< x y = ?
 
-IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
-IsVOrd = ?
+-- IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
+-- IsVOrd = ?