Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/Ordinals.agda @ 923:85f6238a38db
use supf of zchain for (nmx : ¬ Maximal A ) → ⊥
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 19 Oct 2022 08:41:42 +0900 |
parents | a3b7f1e0ca60 |
children | 7c39cae23803 |
line wrap: on
line source
open import Level module Ordinals where open import zf open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Data.Empty open import Relation.Binary.PropositionalEquality open import logic open import nat open import Data.Unit using ( ⊤ ) open import Relation.Nullary open import Relation.Binary open import Relation.Binary.Core record Oprev {n : Level} (ord : Set n) (osuc : ord → ord ) (x : ord ) : Set (suc n) where field oprev : ord oprev=x : osuc oprev ≡ x record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field ordtrans : {x y z : ord } → x o< y → y o< z → x o< z trio< : Trichotomous {n} _≡_ _o<_ ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) <-osuc : { x : ord } → x o< osuc x osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x ) o<-irr : { x y : ord } → ( lt lt1 : x o< y ) → lt ≡ lt1 TransFinite : { ψ : ord → Set (suc n) } → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) → ∀ (x : ord) → ψ x record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where field x<nx : { y : ord } → (y o< next y ) osuc<nx : { x y : ord } → x o< next y → osuc x o< next y ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z)) record Ordinals {n : Level} : Set (suc (suc n)) where field Ordinal : Set n o∅ : Ordinal osuc : Ordinal → Ordinal _o<_ : Ordinal → Ordinal → Set n next : Ordinal → Ordinal isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next isNext : IsNext Ordinal o∅ osuc _o<_ next module inOrdinal {n : Level} (O : Ordinals {n} ) where open Ordinals O open IsOrdinals isOrdinal open IsNext isNext TransFinite0 : { ψ : Ordinal → Set n } → ( (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x ) → ∀ (x : Ordinal) → ψ x TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z) ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))