Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 213:22d435172d1a
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} |