# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674300043 -32400
# Node ID 938ada7fd66c98be9fb18986b4e013d335bd0c37
# Parent  fee9249a2f5053aeb76e204681dd65554fc5223e
Neighbor Filter

diff -r fee9249a2f50 -r 938ada7fd66c src/Topology.agda
--- a/src/Topology.agda	Sat Jan 21 18:30:23 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 20:20:43 2023 +0900
@@ -468,15 +468,29 @@
        P∋limit : odef P limit
        is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v)
 
-Neighbor→F : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x) 
-Neighbor→F {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = ? ; filter2 = ? } where
+NeighborF : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x) 
+NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = ? } where
+    nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v
+    nf00 {v} nei y vy = Neighbor.v⊆P nei vy
     NF : HOD
-    NF = record { od = record { def = λ v → Neighbor TP x v } ; odmax = ? ; <odmax = ? }
+    NF = record { od = record { def = λ v → Neighbor TP x v } ; odmax = & (Power P) ; <odmax = λ lt → odef< (nf00 lt) }
     NF⊆PP : NF ⊆ Power P
-    NF⊆PP = nf00 where
-       nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v
-       nf00 {v} nei y vy = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso)  (Neighbor.ou nei)) ?
-
+    NF⊆PP = nf00 
+    f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q
+    f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; o⊆u = f11 } where
+        f11 :  * (Neighbor.u Np) ⊆ * (& q)
+        f11 {x} ux = subst (λ k → odef k x ) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso (Neighbor.o⊆u Np ux)) )
+    f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q)
+    f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; o⊆u = f20 } where
+         upq : Ordinal
+         upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) )
+         ou : odef (OS TP) upq
+         ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq))
+         ux :  odef (* upq) x
+         ux = subst ( λ k → odef k x ) (sym *iso) ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ 
+         f20 : * upq ⊆ * (& (p ∩ q))
+         f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq 
+           → ⟪ subst (λ k → odef k x) *iso (Neighbor.o⊆u Np (proj1 pq))  , subst (λ k → odef k x) *iso (Neighbor.o⊆u Nq (proj2 pq)) ⟫  )
 -- FIP is UFL
 
 -- filter Base