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

comparison OD.agda @ 213:22d435172d1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate logic and nat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2019 12:17:10 +0900
parents 2c7d45734e3b
children e05575588191
comparison
equal deleted inserted replaced
212:0a1804cc9d0a 213:22d435172d1a
9 open import Data.Empty 9 open import Data.Empty
10 open import Relation.Nullary 10 open import Relation.Nullary
11 open import Relation.Binary 11 open import Relation.Binary
12 open import Relation.Binary.Core 12 open import Relation.Binary.Core
13 13
14 open import logic
15 open import nat
16
14 -- Ordinal Definable Set 17 -- Ordinal Definable Set
15 18
16 record OD {n : Level} : Set (suc n) where 19 record OD {n : Level} : Set (suc n) where
17 field 20 field
18 def : (x : Ordinal {n} ) → Set n 21 def : (x : Ordinal {n} ) → Set n
19 22
20 open OD 23 open OD
21 24
22 open Ordinal 25 open Ordinal
23 open _∧_ 26 open _∧_
27 open _∨_
28 open Bool
24 29
25 record _==_ {n : Level} ( a b : OD {n} ) : Set n where 30 record _==_ {n : Level} ( a b : OD {n} ) : Set n where
26 field 31 field
27 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x 32 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x
28 eq← : ∀ { x : Ordinal {n} } → def b x → def a x 33 eq← : ∀ { x : Ordinal {n} } → def b x → def a x
152 lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy → (ord→od ox) == (ord→od oy) 157 lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy → (ord→od ox) == (ord→od oy)
153 lemma ox ox refl = eq-refl 158 lemma ox ox refl = eq-refl
154 159
155 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y 160 o≡→== : {n : Level} → { x y : Ordinal {n} } → x ≡ y → ord→od x == ord→od y
156 o≡→== {n} {x} {.x} refl = eq-refl 161 o≡→== {n} {x} {.x} refl = eq-refl
157
158 >→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x )
159 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
160 162
161 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x 163 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x
162 c≤-refl x = case1 refl 164 c≤-refl x = case1 refl
163 165
164 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 166 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}