Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1211:f17d060e0bda
UFLP→FIP FIP→UFLP with Zorn done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Mar 2023 11:39:46 +0900 |
| parents | 806109d79562 |
| children | 3922fc5c6f9e |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 64 insertions(+), 63 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Sat Mar 04 10:26:35 2023 +0900 +++ b/src/Tychonoff.agda Sat Mar 04 11:39:46 2023 +0900 @@ -35,10 +35,10 @@ open import filter O open import OPair O open import Topology O --- open import maximum-filter O +open import maximum-filter O -open Filter -open Topology +open Filter +open Topology -- FIP is UFL @@ -56,7 +56,7 @@ field limit : Ordinal P∋limit : odef P limit - is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F + is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v) UFLP→FIP : {P : HOD} (TP : Topology P) → ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP @@ -96,14 +96,14 @@ -- filter base is not empty necessary for generating ultra filter nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X - N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) + N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) ) N∋nc {X} 0<X CSX fip = record { b = X ; x = & e ; b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where e : HOD -- we have an element of X e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) Xe : odef (* X) (& e) Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) - nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) + nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) nn02 : * (& (nc 0<X CSX fip)) ⊆ P nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) ) @@ -140,7 +140,7 @@ → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) -- -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x ) - -- + -- proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅) proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where x≤0 : x o< osuc o∅ @@ -149,21 +149,21 @@ fp00 b y b<X (gi by ) = gi ( b<X by ) fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz) -- - -- then we have maximum ultra filter + -- then we have maximum ultra filter -- - maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) - maxf {X} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) - mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) - mf {X} CSX fp = MaximumFilter.mf (maxf CSX fp) - ultraf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp) - ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) + maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) + maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) + mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) + mf {X} 0<X CSX fp = MaximumFilter.mf (maxf 0<X CSX fp) + ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp) + ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) -- -- so i has a limit as a limit of UIP -- limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal limit {X} CSX fp with trio< o∅ X - ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp)) - ... | tri≈ ¬a 0=X ¬c = o∅ + ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) + ... | tri≈ ¬a 0=X ¬c = o∅ ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) -- -- the limit is an limit of entire elements of X @@ -172,29 +172,29 @@ uf01 {X} CSX fp {x} xx with trio< o∅ X ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx ))) - ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))} - (UFLP.P∋limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))) + ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))} + (UFLP.P∋limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))) ... | case1 lt = lt -- odef (* x) y - ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf CSX fp) uf11 ) where - y = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp)) + ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where + y = UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)) x⊆P : * x ⊆ P x⊆P = cs⊆L TP (CSX (subst (λ k → odef (* X) k) (sym &iso) xx)) uf10 : odef (P ＼ * x ) y uf10 = nlxy uf03 : Neighbor TP y (& (P ＼ * x )) - uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) - ; ux = subst (λ k → odef k y) (sym *iso) uf10 + uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) + ; ux = subst (λ k → odef k y) (sym *iso) uf10 ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz ) - ; u⊆v = λ x → x } - uf07 : * (& (* x , * x)) ⊆ * X + ; u⊆v = λ x → x } + uf07 : * (& (* x , * x)) ⊆ * X uf07 {y} lt with subst (λ k → odef k y) *iso lt ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx - uf05 : odef (filter (MaximumFilter.mf (maxf CSX fp))) x - uf05 = MaximumFilter.F⊆mf (maxf CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 + uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x + uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) ) ; u⊆P = x⊆P ; x⊆u = λ x → x } - uf06 : odef (filter (MaximumFilter.mf (maxf CSX fp))) (& (P ＼ * x )) - uf06 = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp)) uf03 (subst (λ k → odef k y) (sym *iso) uf10) + uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x )) + uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso (UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03 ) uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅ uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) } ) ) where uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y @@ -202,9 +202,9 @@ uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x ))) uf12 z pz with subst (λ k → odef k z) *iso pz ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz - uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅ - uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 - ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12 ) + uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅ + uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅)) + ( filter2 (MaximumFilter.mf (maxf 0<X CSX fp)) (subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) (sym &iso) uf05) uf06 uf12 ) x⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → x ⊆ Cl TP x x⊆Clx {P} TP {x} x<p {y} xy = ⟪ x<p xy , (λ c csc x<c → x<c xy ) ⟫ @@ -213,14 +213,14 @@ FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF -FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 +FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ufl10 ; is-limit = ufl00 } where F∋P : odef (filter F) (& P) F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where fl20 : (P ＼ Ord o∅) =h= P - fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } + fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } 0<P : o∅ o< & P 0<P with trio< o∅ (& P) ... | tri< a ¬b ¬c = a @@ -232,7 +232,7 @@ CF : HOD CF = Replace (filter F) (λ x → Cl TP x ) CF⊆CS : CF ⊆ CS TP - CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) + CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) -- -- it is set of closed set and has FIP ( F is proper ) -- @@ -246,19 +246,19 @@ ufl09 : * z ⊆ P ufl09 {y} zy = f⊆L F az _ zy ufl07 : odef (filter F) x - ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 ) - (subst (λ k → odef (filter F) k) (sym &iso) az) + ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 ) + (subst (λ k → odef (filter F) k) (sym &iso) az) (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) )) F∋sb (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx)) - (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) - (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) ))) + (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) + (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) ))) ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x ufl01 {x} sb = ufl04 where - ufl04 : o∅ o< x - ufl04 with trio< o∅ x + ufl04 : o∅ o< x + ufl04 with trio< o∅ x ... | tri< a ¬b ¬c = a ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) ( - begin + begin x ≡⟨ sym b ⟩ o∅ ≡⟨ sym ord-od∅ ⟩ & od∅ ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) )) where open ≡-Reasoning @@ -266,14 +266,14 @@ ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01) ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11 where ufl11 : odef (* (& CF)) (& P) - ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP))) } + ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP))) } -- -- so we have a limit -- limit : Ordinal - limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 + limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit - ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 + ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 -- -- Neigbor of limit ⊆ Filter -- @@ -281,17 +281,18 @@ -- in (nei : Neighbor TP limit v) , there is an open Set u which contains the limit -- F contains u or P ＼ u because F is ultra -- if F ∋ u, then F ∋ v from u ⊆ v which is a propetery of Neighbor - -- if F ∋ P ＼ u, it is a closed set (Cl (P ＼ u) ≡ P ＼ u) and it does not contains the limit + -- if F ∋ P ＼ u, it is a closed set (Cl (P ＼ u) ≡ P ＼ u) and it does not contains the limit -- this contradicts ufl02 pp : {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei)) - pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz - = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) - ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F - ufl00 {v} nei {x} vx with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei )) - ... | case1 fu = ? where -- Neighbor.u⊆v nei ? where - -- subst (λ k → odef (filter F) k) &iso ( filter1 F ? ? ? ) where - px : Power P ∋ * x - px z xz = Neighbor.v⊆P nei ? + pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz + = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) + ufl00 : {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v + ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei )) + ... | case1 fu = subst (λ k → odef (filter F) k) &iso + ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px) fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where + u = * (Neighbor.u nei) + px : Power P ∋ * v + px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz ) ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where u = * (Neighbor.u nei) P\u : HOD @@ -299,7 +300,7 @@ P\u∋limit : odef P\u limit P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where ufl04 : & P\u ≡ & (Cl TP (* (& P\u))) - ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) + ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))))) ufl03 : odef CF (& P\u ) ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 } @@ -340,14 +341,14 @@ Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) Pf = ? - pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F + pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F pq⊆F = ? - isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F - isL {v} npq {x} fx = ? where + isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v + isL {v} npq = ? where bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) bpq = Neighbor.ou npq (Neighbor.ux npq) pqb : Subbase (pbase TP TQ) (Base.b bpq ) - pqb = Base.sb bpq + pqb = Base.sb bpq pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq ) pqb⊆opq = Base.b⊆u bpq base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → * b ⊆ filter F @@ -356,24 +357,24 @@ -- x is an element of BaseP, which is a subset of Neighbor npq -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp) -- BaseP ∩ F is not empty - -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , + -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , il1 : odef (Power P) z ∧ ZProj1 (filter F) z - il1 = UFLP.is-limit uflp ? bz + il1 = ? -- UFLP.is-limit uflp ? bz nei1 : HOD nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q) plimit : Ordinal - plimit = UFLP.limit uflp + plimit = UFLP.limit uflp nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b nproper = ? b∋z : odef nei1 z b∋z = ? bp : BaseP {P} TP Q z bp = record { p = ? ; op = ? ; prod = ? } - neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F + neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F neip = ? il2 : * z ⊆ ZFP (Power P) (Power Q) il2 = ? - il3 : filter F ∋ ? + il3 : filter F ∋ ? il3 = ? fz : odef (filter F) z fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)