# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688719024 -32400
# Node ID ecfc24f53df46211b58041efe500b1b139170bff
# Parent  11600d5caf37e8f4cc4ef2937eae65f56e08cbce
fix

diff -r 11600d5caf37 -r ecfc24f53df4 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Fri Jul 07 16:41:11 2023 +0900
+++ b/src/Tychonoff.agda	Fri Jul 07 17:37:04 2023 +0900
@@ -35,7 +35,7 @@
 open import filter-util O
 open import ZProduct O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 
 open Filter
 open Topology
@@ -191,11 +191,11 @@
      --    otherwise the check requires a minute
      --
      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)
+     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)
+     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 it has a limit as a limit of FIP
      --