--- a/src/OPair.agda	Thu Dec 29 14:42:28 2022 +0900
+++ b/src/OPair.agda	Fri Dec 30 20:59:14 2022 +0900
@@ -248,6 +248,18 @@
        zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
        ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) 
 
+ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
+ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 
+
+ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
+ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 
 
 
 
+
+
+
+
+
+
+