--- a/HOD.agda	Sun Jun 30 20:31:10 2019 +0900
+++ b/HOD.agda	Sun Jun 30 23:09:17 2019 +0900
@@ -265,6 +265,20 @@
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
 -- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
 
+record Constructible {n : Level} ( α : Ordinal {suc n}) : Set (suc (suc n)) where
+    field
+      LSet : HOD {suc n}
+      L0 :  Def LSet  ∋ LSet 
+      L1 :  {β : Ordinal {suc n}} →  {x : HOD {suc n} } → β o< α   → L β ∋ x → LSet  ∋ x 
+
+open Constructible
+
+Lα : {n : Level} → (α : Ordinal {suc n}) → Constructible {n} α
+Lα {n}  record { lv = Zero ; ord = (Φ .0) } = record { LSet = {!!} ; L0 = {!!} ; L1 = {!!} }
+Lα {n}  record { lv = lx ; ord = (OSuc lv ox) } = record { LSet = {!!} ; L0 = {!!} ; L1 = {!!} }
+Lα {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
+    record { LSet = {!!}  ; L0 = {!!} ; L1 = {!!} }
+
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }