# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674259930 -32400
# Node ID 5e065f0a7ba28d38139522526fa3481145f983ab
# Parent  cd54ee4982493ffc465827527119563e0adf5eba
...

diff -r cd54ee498249 -r 5e065f0a7ba2 src/OPair.agda
--- a/src/OPair.agda	Sat Jan 21 09:02:52 2023 +0900
+++ b/src/OPair.agda	Sat Jan 21 09:12:10 2023 +0900
@@ -254,7 +254,9 @@
 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) )) 
 
-record PProj1 (L : HOD) (x : Ordinal) : Set n where 
+-- simple version 
+
+record ZProj1 (L : HOD) (x : Ordinal) : Set n where 
     field
         pq : Ordinal
         opq : ord-pair pq
@@ -263,16 +265,16 @@
 
 -- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px  ) )))           
 
-Proj1PP : (L P Q : HOD) → HOD
-Proj1PP L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → PProj1 L y) } ; odmax = & P ; <odmax = odef∧< }
+Proj1 : (L P Q : HOD) → HOD
+Proj1 L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → ZProj1 L y) } ; odmax = & P ; <odmax = odef∧< }
    
-record PProj2 (L : HOD) (x : Ordinal) : Set n where 
+record ZProj2 (L : HOD) (x : Ordinal) : Set n where 
     field
         pq : Ordinal
         opq : ord-pair pq
         Lpq : odef L pq    
         x=pi2 : x ≡ pi2 opq
 
-Proj2PP : (L P Q : HOD) → HOD
-Proj2PP L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → PProj2 L y) } ; odmax = & Q ; <odmax = odef∧< }
+Proj2 : (L P Q : HOD) → HOD
+Proj2 L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → ZProj2 L y) } ; odmax = & Q ; <odmax = odef∧< }
    
diff -r cd54ee498249 -r 5e065f0a7ba2 src/Topology.agda
--- a/src/Topology.agda	Sat Jan 21 09:02:52 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 09:12:10 2023 +0900
@@ -553,7 +553,7 @@
 FilterProj  : {P Q LPQ : HOD } 
      → ( LPPQ : LPQ ⊆ Power (ZFP P Q))
      → Filter {LPQ} LPPQ
-     → (Filter {Proj1PP LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2PP LPQ (Power P) (Power Q)} ?) 
+     → (Filter {Proj1 LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2 LPQ (Power P) (Power Q)} ?) 
 FilterProj  = ?
 
 ProuctLimit→ProjLimit  : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  
@@ -583,14 +583,14 @@
              → UFLP (ProductTopology TP TQ) LPQ F UF
      uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
          LP : HOD  -- proj1 of LPQ
-         LP = Proj1PP L (Power P) (Power Q)
+         LP = Proj1 L (Power P) (Power Q)
          LPP : LP ⊆ Power P
          LPP {x} ⟪ Px , p1 ⟫ = Px
          FP : Filter {LP} {P} LPP
-         FP = record { filter = Proj1PP (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj1PP (filter F) (Power P) (Power Q) ⊆ LP
-             ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = PProj1.pq (ppf y)
-                 ; opq = PProj1.opq (ppf y) ; Lpq = f⊆L F (PProj1.Lpq (ppf y)) ; x=pi1 = PProj1.x=pi1 (ppf y) } )  ⟫
+         FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ LP
+             ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = ZProj1.pq (ppf y)
+                 ; opq = ZProj1.opq (ppf y) ; Lpq = f⊆L F (ZProj1.Lpq (ppf y)) ; x=pi1 = ZProj1.x=pi1 (ppf y) } )  ⟫
          UFP : ultra-filter FP
          UFP = record { proper = ? ; ultra = ? }
          uflp : UFLP TP LPP FP UFP