Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff cardinal.agda @ 378:853ead1b56b8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Jul 2020 17:22:16 +0900 |
| parents | 6c72bee25653 |
| children | b737a2e0b46e |
line wrap: on
line diff
--- a/cardinal.agda Mon Jul 20 17:08:16 2020 +0900 +++ b/cardinal.agda Mon Jul 20 17:22:16 2020 +0900 @@ -64,7 +64,7 @@ lemma : Ordinal → Ordinal → Ordinal lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) lemma x y | p | no n = o∅ - lemma x y | p | yes f∋y = lemma2 ? where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) + lemma x y | p | yes f∋y = lemma2 {!!} where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) lemma2 : {p : Ordinal} → ord-pair p → Ordinal lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x) lemma2 (pair x1 y1) | yes p = y1