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

changeset 1442:687a4454fae4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2023 18:11:09 +0900
parents 1a9859a0b14d
children 19f997175d80
files src/cardinal.agda
diffstat 1 files changed, 9 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Tue Jul 04 12:06:12 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 18:11:09 2023 +0900
@@ -361,26 +361,27 @@
          ca01 : odef (Power S) (fun← b x sx )
          ca01 = funA b x sx
 
-     diag2 : {x : Ordinal } → odef S x → (z : Ordinal) → odef (* x) z → odef S z
-     diag2 {x} sx z xz = funA b x sx z ca02 where
-          ca02 : odef (* (fun← b x sx)) z
-          ca02 = ?
+     diag2 : {x : Ordinal } → (sx : odef S x) → (z : Ordinal) → odef (* (fun← b x sx)) z → odef S z
+     diag2 {x} sx z xz = funA b x sx z xz 
      
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x (diag2 sx) ≡ x )
+     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b _ (diag2 sx) ≡ x )
      diagn1 {x} sx dn = ¬t=f (diag sx ) ( begin
            not (diag  sx  )
         ≡⟨⟩
           not ( not (is-S (* (fun← b x sx )) x )) 
         ≡⟨ ? ⟩
-          not (is-S (* (fun← b (fun→ b x (diag2 sx)) (funB b x (diag2 sx) )) ) x )  
+          not (is-S (* (fun← b (fun→ b _ (diag2 sx)) (funB b _ (diag2 sx) )) ) x )  
         ≡⟨ ? ⟩
           not (is-S (* (fun← b x sx )) x)  
         ≡⟨⟩
           diag  sx 
         ∎ ) where open ≡-Reasoning
 
-     diag5 : fun→ b s (diag2 ss) ≡ s
-     diag5 = ?
+     diag5 : fun→ b _ (diag2 ss) ≡ s
+     diag5 = begin
+        fun→ b _ (diag2 ss) ≡⟨ ? ⟩
+        fun→ b _ (λ _ sx → funA b _ ? _  sx) ≡⟨ ? ⟩
+        s ∎ where open ≡-Reasoning
 
      diag4 : ⊥ 
      diag4 = diagn1 ss diag5