Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff src/Topology.agda @ 1182:0727cf865ebd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Fri, 24 Feb 2023 15:00:23 +0800
parents cf25490dd112
children f5deac708524
line wrap: on
line diff
--- a/src/Topology.agda	Fri Feb 24 11:52:44 2023 +0800
+++ b/src/Topology.agda	Fri Feb 24 15:00:23 2023 +0800
@@ -472,8 +472,8 @@
        cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x)
        ... | case1 p = p
        ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where
-          fp04 : {y : Ordinal} → odef (* X) y → Ordinal
-          fp04 {y} xy = & (L ＼ * y)
+          fp04 : {y x : Ordinal} → odef (* X) y → ¬ odef (L ＼ * y) x
+          fp04 {y} {x} xy ⟪ Lx , nx ⟫ = ?
           fp03 : ?
           fp03 = ?
        no-cover : ¬ ( (* (OX CX)) covers L )