Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 43:0d9b9db14361
equalitu and internal parametorisity
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 24 May 2019 22:22:16 +0900 |
| parents | b60db5903f01 |
| children | e584686a1307 |
line wrap: on
line diff
--- a/ordinal.agda Fri May 24 10:28:02 2019 +0900 +++ b/ordinal.agda Fri May 24 22:22:16 2019 +0900 @@ -35,6 +35,9 @@ _o<_ : {n : Level} ( x y : Ordinal ) → Set n _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) +o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x +o<-subst df refl refl = df + open import Data.Nat.Properties open import Data.Empty open import Data.Unit using ( ⊤ )