# HG changeset patch # User Shinji KONO # Date 1672448465 -32400 # Node ID f4c398c60c6758e25c401b4fb026b50e992cb287 # Parent 3b894bbefe92d6213d636cd8b2c18729343309b4 ... diff -r 3b894bbefe92 -r f4c398c60c67 src/Topology.agda --- a/src/Topology.agda Sat Dec 31 00:28:24 2022 +0900 +++ b/src/Topology.agda Sat Dec 31 10:01:05 2022 +0900 @@ -49,6 +49,27 @@ open Topology +-- Base +-- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that +-- W ⊆ U ∩ V and x ∈ W . + +data Subbase (P : HOD) : Ordinal → Set n where + gi : {x : Ordinal } → odef P x → Subbase P x + g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) + +Subases : (P : HOD) → HOD +Subases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ;