--- a/OPair.agda	Tue Jul 14 15:02:59 2020 +0900
+++ b/OPair.agda	Wed Jul 15 08:42:30 2020 +0900
@@ -136,3 +136,18 @@
 p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
+
+_⊗_  : (A B : HOD) → HOD
+A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
+        odmax = pmax; <odmax = <pmax } where
+    checkAB : { p : Ordinal } → def ZFProduct p → Set n
+    checkAB (pair x y) = odef A x ∧ odef B y
+    pmax : Ordinal
+    pmax = omax (odmax A)  (odmax B)
+    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)
+    <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)} ind y where
+        ind : (x : Ordinal)
+            → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B)))
+            → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B))
+        ind = {!!}
+