# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1647166932 -32400
# Node ID be685f338fdc00c3c9cf5e5d3e3072389831e5db
# Parent  81691a6b352b56658b4541a7bcb8d8930bcb57fa
Generic Filter done

diff -r 81691a6b352b -r be685f338fdc src/generic-filter.agda
--- a/src/generic-filter.agda	Sun Mar 13 19:03:33 2022 +0900
+++ b/src/generic-filter.agda	Sun Mar 13 19:22:12 2022 +0900
@@ -185,10 +185,14 @@
            fd = dense-f D p0
            PP∋D : dense D ⊆ Power P
            PP∋D = d⊆P D
+           fd00 : PDHOD P p0 C ∋ p0
+           fd00 = record { gr = 0 ; pn<gr = λ y lt → lt ; x∈PP = Pp0 }
            fd02 : dense D ∋ dense-f D p0 
            fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
+           fd04 : dense-f D p0 ⊆ P
+           fd04 = ODC.power→⊆ O _ _ ( incl PP∋D fd02 )
            fd03 : PDHOD P p0 C  ∋ dense-f D p0 
-           fd03 = f1 {p0} {dense-f D p0} {!!} {!!} ( dense-p D {!!} )
+           fd03 = f1 {p0} {dense-f D p0} fd04 fd00 ( dense-p D (ODC.power→⊆ O _ _ Pp0 ) )
            fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
            fd01 = ⟪ fd02 , fd03 ⟫