Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 58:323b561210b5 | 59:d13d1351a1fa |
|---|---|
| 257 | 257 |
| 258 ∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x | 258 ∅9 : {n : Level} → {x : OD {n} } → ¬ x == od∅ → o∅ o< od→ord x |
| 259 ∅9 {_} {x} not = ∅5 lemma where | 259 ∅9 {_} {x} not = ∅5 lemma where |
| 260 lemma : ¬ od→ord x ≡ o∅ | 260 lemma : ¬ od→ord x ≡ o∅ |
| 261 lemma eq = not ( ∅7 eq ) | 261 lemma eq = not ( ∅7 eq ) |
| 262 | |
| 263 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | |
| 262 | 264 |
| 263 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 265 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
| 264 OD→ZF {n} = record { | 266 OD→ZF {n} = record { |
| 265 ZFSet = OD {suc n} | 267 ZFSet = OD {suc n} |
| 266 ; _∋_ = _∋_ | 268 ; _∋_ = _∋_ |
| 366 lemma d | clt = o<-subst clt ord-iso ord-iso | 368 lemma d | clt = o<-subst clt ord-iso ord-iso |
| 367 ... | () | 369 ... | () |
| 368 reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅ | 370 reg1 : Select (minimul (ord→od x) not) (λ x₁ → (minimul (ord→od x) not ∋ x₁) ∧ ((ord→od x) ∋ x₁)) == od∅ |
| 369 reg1 = record { eq→ = reg0 ; eq← = λ () } where | 371 reg1 = record { eq→ = reg0 ; eq← = λ () } where |
| 370 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) | 372 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) |
| 371 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq where | 373 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq |
| 372 regularity : (x : OD) (not : ¬ (x == od∅)) → | 374 regularity : (x : OD) (not : ¬ (x == od∅)) → |
| 373 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) | 375 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
| 374 proj1 (regularity x not ) = minimul<x x not | 376 regularity x not = |
| 375 proj2 (regularity x not ) = record { eq→ = reg4 ; eq← = λ () } where | 377 subst₂ ( λ x min → (x ∋ min) ∧ (Select min (λ x₁ → (min ∋ x₁) ∧ (x ∋ x₁)) == od∅) ) |
| 376 reg4 : {xd : Ordinal } → def (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁))) xd → def od∅ xd | 378 oiso lemma ( regularity-ord (od→ord x) (subst (λ k → ¬ (k == od∅) ) (sym oiso) not )) where |
| 377 reg4 {xd} = {!!} (eq→ (proj1 (regularity-ord {!!} {!!} )) ) | 379 lemma : minimul (ord→od (od→ord x)) (subst (λ k → ¬ (k == od∅)) (sym oiso) not) ≡ minimul x not |
| 378 | 380 lemma = cong₂ (λ x not → minimul x not ) oiso {!!} |
| 379 | 381 |
| 380 | 382 |
| 381 | 383 |
| 382 | 384 |
| 385 | |
| 386 |