Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
42:4d5fc6381546 | 43:0d9b9db14361 |
---|---|
32 | 32 |
33 open Ordinal | 33 open Ordinal |
34 | 34 |
35 _o<_ : {n : Level} ( x y : Ordinal ) → Set n | 35 _o<_ : {n : Level} ( x y : Ordinal ) → Set n |
36 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) | 36 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) |
37 | |
38 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x | |
39 o<-subst df refl refl = df | |
37 | 40 |
38 open import Data.Nat.Properties | 41 open import Data.Nat.Properties |
39 open import Data.Empty | 42 open import Data.Empty |
40 open import Data.Unit using ( ⊤ ) | 43 open import Data.Unit using ( ⊤ ) |
41 open import Relation.Nullary | 44 open import Relation.Nullary |