annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
1 {-# OPTIONS --allow-unsolved-metas #-}
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
2 open import Level
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
3 module ordinal where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
5 open import zf
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
9 open import Relation.Binary.PropositionalEquality
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
11 data OrdinalD {n : Level} : (lv : Nat) → Set n where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
12 Φ : (lv : Nat) → OrdinalD lv
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
13 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
14 ℵ_ : (lv : Nat) → OrdinalD (Suc lv)
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
16 record Ordinal {n : Level} : Set n where
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
17 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
18 lv : Nat
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
19 ord : OrdinalD {n} lv
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
20
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
21 data ¬ℵ {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
22 ¬ℵΦ : ¬ℵ (Φ lx)
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
23 ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x)
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
24
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
25 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
26 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
27 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
28 ℵΦ< : {lx : Nat} → Φ (Suc lx) d< (ℵ lx)
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
29 ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x → OSuc (Suc lx) x d< (ℵ lx)
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
30 ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx)
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
31 ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
32
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
33 open Ordinal
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
34
27
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
35 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
36 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
38 o<-subst : {n : Level } {Z X z x : Ordinal {n}} → Z o< X → Z ≡ z → X ≡ x → z o< x
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
39 o<-subst df refl refl = df
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 41
diff changeset
40
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
41 open import Data.Nat.Properties
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
42 open import Data.Empty
30
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
43 open import Data.Unit using ( ⊤ )
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
44 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
45
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
46 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
47 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
48
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
49 o∅ : {n : Level} → Ordinal {n}
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
50 o∅ = record { lv = Zero ; ord = Φ Zero }
21
6d9fdd1dfa79 add transfinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
51
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
52 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
53 s<refl {n} {lv} {Φ lv} = Φ<
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
54 s<refl {n} {lv} {OSuc lv x} = s< s<refl
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
55 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
56
39
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
57 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
58
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
59 ordinal-cong : {n : Level} {x y : Ordinal {n}} →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
60 lv x ≡ lv y → ord x ≅ ord y → x ≡ y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 35
diff changeset
61 ordinal-cong refl refl = refl
21
6d9fdd1dfa79 add transfinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
62
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
63 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
64 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
65
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
66 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
67 trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
68 trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ())
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
69 trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs<
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
70 trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
71 trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< ()
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
72 trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ())
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
73 trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
74 trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
75 trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x)
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
76
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
77 trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
78 trio<≡ refl = ≡→¬d<
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
79
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
80 trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
81 trio>≡ refl = ≡→¬d<
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
82
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
83 triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
84 triO {n} {lx} {ly} x y = <-cmp lx ly
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
85
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
86 fin : {n : Level} → {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
87 fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
88 fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
89
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
90 triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} )
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
91 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
92 triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
93 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
94 triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< ℵΦ< (λ ()) ( λ lt → trio<> lt ℵΦ<)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
95 triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ<
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
96 triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
97 triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
98 triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri< ℵs< (λ ()) ( λ lt → trio<> lt ℵs< )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
99 triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c)) ) (λ ()) ( ℵ< (fin c) )
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
100 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
101 triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
102 triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) ( λ lt → trio<> lt (ℵ< (fin a )))
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
103 triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs<
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
104 triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c )) (λ ()) ( ℵss< c )
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
105 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
106 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) )
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
107 triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
108 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
109
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
110 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
111 d<→lv Φ< = refl
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
112 d<→lv (s< lt) = refl
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
113 d<→lv ℵΦ< = refl
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
114 d<→lv (ℵ< _) = refl
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
115 d<→lv ℵs< = refl
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
116 d<→lv (ℵss< _) = refl
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
117
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
118 xsyℵ : {n : Level} {lx : Nat} {x y : OrdinalD {n} lx } → x d< y → ¬ℵ y → ¬ℵ x
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
119 xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
120 xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
121 xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) ()
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
122 xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
123 xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
124 xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
125
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
126 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
127 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ<
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
128 orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ<
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
129 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
34
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
130 orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ)
c9ad0d97ce41 fix oridinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 33
diff changeset
131 orddtrans ℵs< (ℵ< ())
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
132 orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
133 orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ<
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
134 orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s< ℵΦ<
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
135 orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
136 orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs<
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
137 orddtrans ℵΦ< (ℵss< y<z) = Φ<
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
138 orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ< y<z)
35
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
139 orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
140 orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
141 orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
142 orddtrans (ℵss< ()) (ℵ< ¬ℵΦ)
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
143 orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ()))
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
144 orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x )
88b77cecaeba ordinal fixed
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
145 orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z )
9
5ed16e2d8eb7 try to fix axiom of replacement
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
146
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
147 max : (x y : Nat) → Nat
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
148 max Zero Zero = Zero
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
149 max Zero (Suc x) = (Suc x)
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
150 max (Suc x) Zero = (Suc x)
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
151 max (Suc x) (Suc y) = Suc ( max x y )
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
153 maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
154 maxαd x y with triOrdd x y
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
155 maxαd x y | tri< a ¬b ¬c = y
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
156 maxαd x y | tri≈ ¬a b ¬c = x
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
157 maxαd x y | tri> ¬a ¬b c = x
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
158
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
159 maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
160 maxα x y with <-cmp (lv x) (lv y)
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
161 maxα x y | tri< a ¬b ¬c = x
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
162 maxα x y | tri> ¬a ¬b c = y
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
163 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
7
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 6
diff changeset
164
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
165 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
166 a o≤ b = (a ≡ b) ∨ ( a o< b )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
167
27
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
168 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
169 ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
170 ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
171 ... | refl = case1 x₁
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
172 ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
173 ... | refl = case1 x₂
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
174 ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
175 ... | refl | refl = case2 ( orddtrans x₁ x₂ )
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
176
bade0a35fdd9 OD, HOD, TC
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 26
diff changeset
177
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
178 trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
179 trio< a b with <-cmp (lv a) (lv b)
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
180 trio< a b | tri< a₁ ¬b ¬c = tri< (case1 a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
181 lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
182 lemma1 (case1 x) = ¬c x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
183 lemma1 (case2 x) with d<→lv x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
184 lemma1 (case2 x) | refl = ¬b refl
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
185 trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
186 lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
187 lemma1 (case1 x) = ¬a x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
188 lemma1 (case2 x) with d<→lv x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
189 lemma1 (case2 x) | refl = ¬b refl
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
190 trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
191 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
192 lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
193 lemma1 refl = refl
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
194 lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
195 lemma2 (case1 x) = ¬a x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
196 lemma2 (case2 x) = trio<> x a
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
197 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
198 lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
199 lemma1 refl = refl
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
200 lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
201 lemma2 (case1 x) = ¬a x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
202 lemma2 (case2 x) = trio<> x c
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
203 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
204 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
205 lemma1 (case1 x) = ¬a x
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
206 lemma1 (case2 x) = ≡→¬d< x
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
207
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
208 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
209 OrdTrans (case1 refl) (case1 refl) = case1 refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
210 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
211 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
17
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
212 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
213 OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
214 OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
215 OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
216 OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
217 OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
6a668c6086a5 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
218 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
219
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
220 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
221 OrdPreorder {n} = record { Carrier = Ordinal
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
222 ; _≈_ = _≡_
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
223 ; _∼_ = _o≤_
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
224 ; isPreorder = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
225 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
226 ; reflexive = case1
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
227 ; trans = OrdTrans
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
228 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
229 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
230
30
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
231 TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
22
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
232 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } ))
24
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
233 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
3186bbee99dd separte level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 23
diff changeset
234 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
22
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
235 → ∀ (x : Ordinal) → ψ x
30
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
236 TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
237 TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
238 ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
3b0fdb95618e problem on Ordinal ( OSuc ℵ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 29
diff changeset
239 TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
22
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
240