Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 59:d13d1351a1fa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
files ordinal-definable.agda
diffstat 1 files changed, 9 insertions(+), 5 deletions(-) [+]
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 {!!}
+