Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 146:2eafa89733ed
ord-Ord causes od→ord x o< od→ord y → y ∋ x,
it makes y ∋ φ
dead end
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 18:26:33 +0900 |
| parents | f0fa9a755513 |
| children | c848550c8b39 |
| files | HOD.agda |
| diffstat | 1 files changed, 3 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 08 18:19:56 2019 +0900 +++ b/HOD.agda Mon Jul 08 18:26:33 2019 +0900 @@ -102,6 +102,9 @@ o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt +o<→c<' : {n : Level} {x y : OD {suc n} } → od→ord x o< od→ord y → y ∋ x +o<→c<' {n} {x} {y} lt = def-subst {suc n} {Ord (od→ord y)} {od→ord x} {y} {od→ord x} lt Ord-ord-≡ refl + sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )