--- a/constructible-set.agda	Tue May 14 03:38:26 2019 +0900
+++ b/constructible-set.agda	Tue May 14 03:52:42 2019 +0900
@@ -88,26 +88,14 @@
 max (Suc x) Zero = (Suc x)
 max (Suc x) (Suc y) = Suc ( max x y )
 
-lvconv : { lx ly : Nat } → lx > ly → lx ≡ (max lx ly)
-lvconv {Zero} {Zero} ()
-lvconv {Zero} {Suc ly} ()
-lvconv {Suc lx} {Zero} (s≤s lt) = refl
-lvconv {Suc lx} {Suc ly} (s≤s lt) = cong ( λ x → Suc x ) ( lvconv lt )
+maxα> : {n : Level } → { lx ly : Nat } → Ordinal {n} lx  →  Ordinal {n} ly  → lx > ly  → Ordinal {n} lx
+maxα> x y _ = x
 
-olconv : {n : Level } → { lx ly : Nat } → Ordinal {n} ly  → lx < ly  →  Ordinal {n} (max lx ly) 
-olconv {n} {lx} {ly} (Φ {x}) lt = Φ
-olconv {n} {lx} {ly} (T-suc x) lt = T-suc (olconv x lt)
-olconv {n} {lx} {Suc lv} (ℵ lv) lt = {!!}
-
-maxα : {n : Level } → { lx ly : Nat } → Ordinal {n} lx  →  Ordinal {n} ly  → Ordinal {n} (max lx ly)
-maxα x y with triO x y
-maxα Φ y | tri< a ¬b ¬c = Φ
-maxα (T-suc x) y | tri< a ¬b ¬c = olconv x a
-maxα (ℵ lv) y | tri< a ¬b ¬c = {!!}
-maxα x y | tri> ¬a ¬b c = {!!}
-maxα Φ y | tri≈ ¬a b ¬c = Φ
-maxα (T-suc x) y | tri≈ ¬a b ¬c = T-suc  {!!}
-maxα (ℵ lv) y | tri≈ ¬a b ¬c = {!!}
+maxα= : {n : Level } → { lx : Nat } → Ordinal {n} lx  →  Ordinal {n} lx  →  Ordinal {n} lx
+maxα= x y with triOonSameLevel x y
+maxα= x y | tri< a ¬b ¬c = y
+maxα= x y | tri≈ ¬a b ¬c = x
+maxα= x y | tri> ¬a ¬b c = x
 
 -- X' = { x ∈ X |  ψ  x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
 
@@ -124,7 +112,7 @@
 open ConstructibleSet
 
 data _c∋_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } →
-    Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
+        Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
     c> : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' }
         (ta : Constructible {n} {lv} α ) ( tx : Constructible {n} {lv'} α' ) → α' o< α →  ta c∋ tx
     xself-fsub  : {lv : Nat} {α : Ordinal {n} lv } 
@@ -136,10 +124,13 @@
 _∋_  : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n 
 a ∋ x  = constructible a c∋ constructible x
 
+transitiveness : {n : Level} → (a b c : ConstructibleSet {n}) → a ∋ b → b ∋ c → a ∋ c
+transitiveness = {!!}
+
 data _c≈_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } →
-    Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
-        crefl :  {lv : Nat} {α : Ordinal {n} lv } → _c≈_ {n} {_} {_} {α} {α} (xself α ) (xself α )
-        feq :  {lv : Nat} {α : Ordinal {n} lv }
+        Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where
+    crefl :  {lv : Nat} {α : Ordinal {n} lv } → _c≈_ {n} {_} {_} {α} {α} (xself α ) (xself α )
+    feq :  {lv : Nat} {α : Ordinal {n} lv }
           → ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) 
           → (∀ ( x :  Ordinal {n} lv ) → ψ x  ⇔ ψ₁ x ) → _c≈_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁)