diff OD.agda @ 387:8b0715e28b33

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Jul 2020 09:09:00 +0900
parents d2cb5278e46d
children 19687f3304c9
line wrap: on
line diff
--- a/OD.agda	Thu Jul 23 17:50:28 2020 +0900
+++ b/OD.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -76,9 +76,6 @@
 --
 --  ==→o≡ is necessary to prove axiom of extensionality.
 
-data One {n : Level } : Set n where
-  OneObj : One
-
 -- Ordinals in OD , the maximum
 Ords : OD
 Ords = record { def = λ x → One }
@@ -274,6 +271,12 @@
 open _⊆_
 infixr  220 _⊆_
 
+trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
+
+refl-⊆ : {A : HOD} → A ⊆ A
+refl-⊆ {A} = record { incl = λ x → x }
+
 od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
 od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
 
@@ -317,14 +320,14 @@
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
 -- level trick (what'a shame)
-ε-induction1 : { ψ : HOD  → Set (suc n)}
-   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : HOD ) → ψ x
-ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
-     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
-     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
-     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
-     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+-- ε-induction1 : { ψ : HOD  → Set (suc n)}
+--    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+--    → (x : HOD ) → ψ x
+-- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+--      induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+--      induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+--      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+--      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }