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

comparison src/VL.agda @ 1476:32001d93755b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 28 Jun 2024 20:55:38 +0900
parents 171c3f3cdc6b
children
comparison
equal deleted inserted replaced
1475:6752e2ff4dc6 1476:32001d93755b
1 {-# OPTIONS --cubical-compatible --safe #-}
1 open import Level 2 open import Level
2 open import Ordinals 3 open import Ordinals
3 module VL {n : Level } (O : Ordinals {n}) where 4 open import logic
5 open import Relation.Nullary
6
7 open import Level
8 open import Ordinals
9 import HODBase
10 import OD
11 open import Relation.Nullary
12 module VL {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where
13
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
15 open import Data.Empty
16
17 import OrdUtil
18
19 open Ordinals.Ordinals O
20 open Ordinals.IsOrdinals isOrdinal
21 import ODUtil
4 22
5 open import logic 23 open import logic
6 import OD 24 open import nat
7 open import Relation.Nullary 25
8 open import Relation.Binary
9 open import Data.Empty
10 open import Relation.Binary
11 open import Relation.Binary.Core
12 open import Relation.Binary.PropositionalEquality
13 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14 import BAlgebra
15 open BAlgebra O
16 open inOrdinal O
17 import OrdUtil
18 import ODUtil
19 open Ordinals.Ordinals O
20 open Ordinals.IsOrdinals isOrdinal
21 -- open Ordinals.IsNext isNext
22 open OrdUtil O 26 open OrdUtil O
23 open ODUtil O 27 open ODUtil O HODAxiom ho<
24 28
25 open OD O
26 open OD.OD
27 open ODAxiom odAxiom
28 -- import ODC
29 open _∧_ 29 open _∧_
30 open _∨_ 30 open _∨_
31 open Bool 31 open Bool
32 open HOD 32
33 open HODBase._==_
34
35 open HODBase.ODAxiom HODAxiom
36 open OD O HODAxiom
37
38 open HODBase.HOD
39
40
41 open import Relation.Nullary
42 open import Relation.Binary
43 open import Data.Empty
44 open import Relation.Binary
45 open import Relation.Binary.Core
46 open import Relation.Binary.PropositionalEquality
47 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
48
33 49
34 -- The cumulative hierarchy 50 -- The cumulative hierarchy
35 -- V 0 := ∅ 51 -- V 0 := ∅
36 -- V α + 1 := P ( V α ) 52 -- V α + 1 := P ( V α )
37 -- V α := ⋃ { V β | β < α } 53 -- V α := ⋃ { V β | β < α }
57 field 73 field
58 x : Ordinal 74 x : Ordinal
59 β : Ordinal 75 β : Ordinal
60 ov : odef (TransFinite V1 β) x 76 ov : odef (TransFinite V1 β) x
61 77
62 Vn∅ : Vn 78 -- Vn∅ : Vn
63 Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? } 79 -- Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
64 80
65 vsuc : Vn → Vn 81 -- vsuc : Vn → Vn
66 vsuc v = ? 82 -- vsuc v = ?
67 83
68 v< : Vn → Vn → Set n 84 -- v< : Vn → Vn → Set n
69 v< x y = ? 85 -- v< x y = ?
70 86
71 IsVOrd : IsOrdinals Vn Vn∅ vsuc ? 87 -- IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
72 IsVOrd = ? 88 -- IsVOrd = ?
73 89