# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649802382 -32400
# Node ID 5dd9cf0094d53fc9defdf44463e7c81ada149b8f
# Parent  1546541ed4618b752fed750e363c6746186c0b59
...

diff -r 1546541ed461 -r 5dd9cf0094d5 src/zorn.agda
--- a/src/zorn.agda	Tue Apr 12 18:52:14 2022 +0900
+++ b/src/zorn.agda	Wed Apr 13 07:26:22 2022 +0900
@@ -88,6 +88,25 @@
 me : { A a : HOD } → A ∋ a → Element A
 me {A} {a} lt = record { elm = a ; is-elm = lt }
 
+A∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (A ∋ x) ≡ (A ∋ y )
+A∋x-irr A {x} {y} refl = refl
+
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
+postulate
+   ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay 
+   odef-irr : (A : OD) {x y : Ordinal} → x ≡ y → (ax : def A x) (ay : def A y ) → ax ≅ ay 
+
+is-elm-irr : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y 
+is-elm-irr A {x} {y} eq = ∋x-irr A eq (is-elm x) (is-elm y )
+
+El-irr2 : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y → x ≡ y
+El-irr2  A {x} {y} refl HE.refl = refl
+
+El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
+El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
+
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (suc n) where
    field
       max : HOD
@@ -157,9 +176,29 @@
         ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A  (proj1 lt) ))  }
     zc2 :  OSup> A (d→∋ A (is-elm x))  ∨ Maximal A ∨ InFiniteIChain A  (d→∋ A (is-elm x))
     zc2 with  is-o∅ (& Gtx)
-    ... | no nogt = case1 {!!}
+    ... | no not = case1 record { y = & y ; icy = zc4 ; y>x = proj2 zc3 } where
+        y : HOD
+        y =  ODC.minimal O Gtx  (λ eq → not (=od∅→≡o∅ eq))
+        zc3 :  odef ( IChainSet x ) (& y) ∧  ( & (elm x) o< (& y ))
+        zc3  = ODC.x∋minimal O Gtx  (λ eq → not (=od∅→≡o∅ eq))
+        zc4 : odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) (is-elm x)))) (& y)
+        zc4 = ⟪ proj1 (proj1 zc3) , (λ ic → zc6 (* (& (elm x))) (sym *iso) ic) ⟫ where 
+          zc5 : odef (IChainSet (me (is-elm x))) (& y)
+          zc5 = proj1 zc3
+          zc6 : (ax : HOD) → elm x ≡ ax → (iy : IChain A (& y)) →  ic-connet iy  (& ax)
+          zc6 ax refl iy = proj2 (proj1 zc3) iy
     ... | yes nogt with is-o∅ (& HG)
-    ... | no  nohg = case2 (case1 {!!} )
+    ... | no  nohg = case2 (case1 record { maximal = y ; A∋maximal = proj1 zc3 ; ¬maximal<x = zc4 } ) where
+        y : HOD
+        y =  ODC.minimal O HG (λ eq → nohg (=od∅→≡o∅ eq))
+        zc3 :  odef A (& y) ∧ IsFC A (d→∋ A (is-elm x) ) (& y)
+        zc3  = ODC.x∋minimal O HG  (λ eq → nohg (=od∅→≡o∅ eq))
+        zc5 : odef (IChainSet {A} (me (d→∋ A (is-elm x) ))) (& y)
+        zc5 = IsFC.icy (proj2 zc3)
+        zc6 :  odef (IChainSet {IChainSet (me (d→∋ A (is-elm x)))} (me (d→∋ (IChainSet (me (d→∋ A (is-elm x)))) (IsFC.icy (proj2 zc3))))) (& y)
+        zc6 = ⟪ {!!} , {!!} ⟫
+        zc4 : {z : HOD} → A ∋ z → ¬ (y < z)
+        zc4 {z} az y<z = IsFC.c-finite (proj2 zc3) record { y = & z ; icy =  {!!} ; y>x = {!!} }
     ... | yes  nohg = case2 (case2 {!!} )