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

changeset 1420:836bcc102a2c

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 Sat, 01 Jul 2023 07:44:45 +0900
parents 2da55d442e4f
children cdfe297f9a79
files src/cardinal.agda
diffstat 1 files changed, 15 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Sat Jul 01 06:19:03 2023 +0900
+++ b/src/cardinal.agda	Sat Jul 01 07:44:45 2023 +0900
@@ -299,6 +299,10 @@
             ... | a-g ax ¬ib = sym x=fy
             ... | next-gf t ix = sym x=fy
 
+      UC-iso11 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a  f)))) x ) 
+         → (ux : odef (* (& UC)) (Uf x cx)) → fU ( Uf x cx ) ux  ≡ x
+      UC-iso11 x cx ux = subst (λ k → fU (Uf x cx) k ≡ x) ( HE.≅-to-≡ ( ∋-irr {* (& UC)} {_} (be08 cx) ux)) (UC-iso1 x cx)
+
       CC0 : (x : Ordinal) → Set n
       CC0 x =  gfImage x ∨ (¬ gfImage x) 
 
@@ -387,15 +391,18 @@
       ... | case1 lt1 = ?
       ... | case2 lt1 = ?
 
+      ImageInject : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j
+      ImageInject {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j))
+
       be72 :  (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) →  h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x
-      be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = subst (λ k → fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) k ≡ x) 
-        ? be76 where
-          be77 : odef (* (& UC)) (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) ≅ be08 (subst (λ k → odef k x) (sym *iso) x₁)
-          be77 = ?
-          be76 : fU (Uf x (subst (λ k → odef k x) (sym *iso) x₁)) (be08 (subst (λ k → odef k x) (sym *iso) x₁)) ≡ x
-          be76 = UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁)
-      -- ... | case1 c1 = ? -- trans ? (UC-iso1 x (subst (λ k → odef k x) (sym *iso) x₁))
-      -- ... | case2 c2 = ⊥-elim ( c2 ? )
+      be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = UC-iso11 x be76 
+                  (subst (λ k → odef k (IsImage.y (subst (λ k → odef k x) *iso be76))) (sym *iso) be77 ) where
+           be76 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x
+           be76 = subst (λ k → odef k x) (sym *iso) x₁
+           be78 : y ≡ IsImage.y (subst (λ k → odef k x) *iso be76)
+           be78 = ImageInject x₁ (subst (λ k → odef k x) *iso be76)
+           be77 : odef UC (IsImage.y (subst (λ k → odef k x) *iso be76))
+           be77 = subst₂ (λ j k → odef j k ) *iso be78 ay 
       be72 x bx (case2 x₁)  with cc10 bx (case2 x₁)
       ... | case1 c1 = ⊥-elim ( x₁ ? )
       ... | case2 c2 = trans ? (a-UC-iso1 x ? )