# HG changeset patch # User Shinji KONO # Date 1595651633 -32400 # Node ID d58edc4133b01069c362e92111776fc3698c4198 # Parent cb183674facfd1f25ede6f1634ac37087aa61163 generic filter diff -r cb183674facf -r d58edc4133b0 generic-filter.agda --- a/generic-filter.agda Sat Jul 25 13:12:29 2020 +0900 +++ b/generic-filter.agda Sat Jul 25 13:33:53 2020 +0900 @@ -162,12 +162,12 @@ record CountableHOD : Set (suc (suc n)) where field - phod : HOD - ptl→ : Nat → Ordinal - ptl→∈P : (i : Nat) → odef phod (ptl→ i) - ptl← : (x : Ordinal) → odef phod x → Nat - ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x - ptl-iso← : { x : Nat } → ptl← (ptl→ x ) (ptl→∈P x) ≡ x + mhod : HOD + mtl→ : Nat → Ordinal + mtl→∈P : (i : Nat) → odef mhod (mtl→ i) + mtl← : (x : Ordinal) → odef mhod x → Nat + mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x + mtl-iso← : { x : Nat } → mtl← (mtl→ x ) (mtl→∈P x) ≡ x open CountableOrdinal @@ -177,47 +177,36 @@ PGHOD i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (ord→od p) y → odef (ord→od x) y ) } ; odmax = ctl→ C i ;