Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 59:d13d1351a1fa
lemma = cong₂ (λ x not → minimul x not ) oiso { }6
Cannot instantiate the metavariable _1342 to solution (x == od∅ →
⊥) since it contains the variable x which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 May 2019 05:46:05 +0900 |
| parents | 323b561210b5 |
| children | 6a1f67a4cc6e |
line wrap: on
line diff
--- a/ordinal-definable.agda Tue May 28 23:02:50 2019 +0900 +++ b/ordinal-definable.agda Wed May 29 05:46:05 2019 +0900 @@ -260,6 +260,8 @@ lemma : ¬ od→ord x ≡ o∅ lemma eq = not ( ∅7 eq ) +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} OD→ZF {n} = record { ZFSet = OD {suc n} @@ -368,13 +370,15 @@ reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅ reg1 = record { eq→ = reg0 ; eq← = λ () } where ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) - ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq where + ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) - proj1 (regularity x not ) = minimul<x x not - proj2 (regularity x not ) = record { eq→ = reg4 ; eq← = λ () } where - reg4 : {xd : Ordinal } → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) xd → def od∅ xd - reg4 {xd} = {!!} (eq→ (proj1 (regularity-ord {!!} {!!} )) ) + regularity x not = + subst₂ ( λ x min → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) ) + oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where + lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not + lemma = cong₂ (λ x not → minimul x not ) oiso {!!} +