# HG changeset patch # User Shinji KONO # Date 1688197657 -32400 # Node ID a2b59bbe5eef54e9df1175af417e73839a7408d0 # Parent 2134c62fdc30c1c0947de5ae5164550031cf9896 ... diff -r 2134c62fdc30 -r a2b59bbe5eef src/cardinal.agda --- a/src/cardinal.agda Sat Jul 01 16:13:27 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 16:47:37 2023 +0900 @@ -423,16 +423,18 @@ ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) }) - ... | case2 c2 = a-UC-iso11 x be76 be78 where - be76 : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x - be76 = subst (λ k → odef k x) (sym *iso) ⟪ bx , (λ lt → subst (λ k → odef k x → ⊥) (sym *iso) x₁ lt ) ⟫ - be78 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76))) - be78 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)))) - (sym *iso) ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x - (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso) - ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso) - ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) - ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , ? ⟫)) , c2 ⟫ + ... | case2 c2 with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) + (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) ))) ) + ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫) )) ? ? ) + ... | case2 nimg = ? + -- = trans (g⁻¹-eq _ (be15 be51) {_} {be16 be51}) be50 where + -- be52 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x + -- be52 = subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫ + -- be51 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52))) + -- be51 = subst (λ k → odef k (fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52)))) (sym *iso) + -- ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso be52)) , ? ⟫ + -- be50 : g⁻¹ (be15 be51) (be16 be51) ≡ x + -- be50 = ? be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) → h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x