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

comparison ordinal.agda @ 43:0d9b9db14361

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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