Mercurial > hg > Members > kono > Proof > ZF-in-agda
view VL.agda @ 414:aa306f5dab9b
add VL
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 30 Jul 2020 16:06:36 +0900 |
parents | |
children | 3dda56a5befd |
line wrap: on
line source
open import Level open import Ordinals module VL {n : Level } (O : Ordinals {n}) where open import zf open import logic import OD open import Relation.Nullary open import Relation.Binary open import Data.Empty open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) import BAlgbra open BAlgbra O open inOrdinal O open OD O open OD.OD open ODAxiom odAxiom -- import ODC open _∧_ open _∨_ open Bool open HOD -- The cumulative hierarchy -- V 0 := ∅ . -- V β + 1 := P ( V β ) . -- V λ := ⋃ β < λ V β . {-# TERMINATING #-} V : ( β : Ordinal ) → HOD V β = TransFinite1 Vβ₁ β where Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD Vβ₁ x Vβ₀ with trio< x o∅ Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a) Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = od∅ Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p x Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc )) Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p = Vβ<α x where Vβ<α : (α : Ordinal ) → HOD Vβ<α α = record { od = record { def = λ x → (x o< α ) ∧ odef (V x) x } ; odmax = α; <odmax = λ {x} lt → proj1 lt }