# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655468424 -32400
# Node ID 099ca2fea51c8fc83f892450b7017079168e506f
# Parent  d6ad1af5299ec5de204d2d2e67f8596b7d506863
...

diff -r d6ad1af5299e -r 099ca2fea51c src/OD.agda
--- a/src/OD.agda	Fri Jun 17 18:45:08 2022 +0900
+++ b/src/OD.agda	Fri Jun 17 21:20:24 2022 +0900
@@ -215,8 +215,6 @@
 ≡od∅→=od∅  : {x : HOD} → x ≡ od∅ → od x == od od∅
 ≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x  ≡ k ) ord-od∅ ( cong & eq ) )
 
--- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
-
 ∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
diff -r d6ad1af5299e -r 099ca2fea51c src/Ordinals.agda
--- a/src/Ordinals.agda	Fri Jun 17 18:45:08 2022 +0900
+++ b/src/Ordinals.agda	Fri Jun 17 21:20:24 2022 +0900
@@ -26,6 +26,7 @@
      <-osuc   : { x : ord  } → x o< osuc x
      osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
      Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
+     o<-irr   : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1
      TransFinite : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
diff -r d6ad1af5299e -r 099ca2fea51c src/ordinal.agda
--- a/src/ordinal.agda	Fri Jun 17 18:45:08 2022 +0900
+++ b/src/ordinal.agda	Fri Jun 17 21:20:24 2022 +0900
@@ -200,6 +200,17 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
+open import Data.Nat.Properties as DP
+OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
+OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
+OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
+OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
+      lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
+      lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
+      lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
+ 
 open import Ordinals 
 
 C-Ordinal : {n : Level} →  Ordinals {suc n} 
@@ -216,6 +227,7 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite2
+     ; o<-irr = OrdIrr
      ; Oprev-p  = Oprev-p 
    } ;
    isNext = record {
diff -r d6ad1af5299e -r 099ca2fea51c src/zorn.agda
--- a/src/zorn.agda	Fri Jun 17 18:45:08 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 21:20:24 2022 +0900
@@ -667,8 +667,7 @@
          ... | tri> ¬a ¬b c = sym *iso
          seq<x : {b : Ordinal } → (b<x : b o< x ) →  * (SupF.chain (ZChain1.supf (prev b b<x {y} ay) b))  ≡ * (SupF.chain (supf0 b))
          seq<x {b} b<x with trio< b x
-         ... | tri< a ¬b ¬c = ==→o≡ record { eq→ = ? ; eq← = ? }
-         --  cong (λ k → * (SupF.chain (ZChain1.supf (prev b k {y} ay) b)) ) {!!} --  b<x ≡ a
+         ... | tri< a ¬b ¬c = cong (λ k → * (SupF.chain (ZChain1.supf (prev b k {y} ay) b)) ) o<-irr --  b<x ≡ a
          ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
          ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
          u-mono :  ( a b : Ordinal ) → b o< x → a o< osuc b → (za : ZChain1 A y f a) (zb : ZChain1 A y f b) → ZChain.chain (ZChain1.zc za)  ⊆' ZChain.chain (ZChain1.zc zb)