# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719720300 -32400
# Node ID 42df464988e83e32c169c567253a5af764b65fc6
# Parent  ba406e2ba8af6d519b35b713882e91523ff18e7f
o<-irr reintroduce

diff -r ba406e2ba8af -r 42df464988e8 src/Ordinals.agda
--- a/src/Ordinals.agda	Sun Jun 30 11:03:33 2024 +0900
+++ b/src/Ordinals.agda	Sun Jun 30 13:05:00 2024 +0900
@@ -26,7 +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
+     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 ba406e2ba8af -r 42df464988e8 src/ordinal.agda
--- a/src/ordinal.agda	Sun Jun 30 11:03:33 2024 +0900
+++ b/src/ordinal.agda	Sun Jun 30 13:05:00 2024 +0900
@@ -225,6 +225,7 @@
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite2
      ; Oprev-p  = Oprev-p
+     ; o<-irr = OrdIrr _ _
    } --
    -- isNext = record {
    --     x<nx = x<nx
diff -r ba406e2ba8af -r 42df464988e8 src/zorn.agda
--- a/src/zorn.agda	Sun Jun 30 11:03:33 2024 +0900
+++ b/src/zorn.agda	Sun Jun 30 13:05:00 2024 +0900
@@ -1224,7 +1224,8 @@
                fc12 = ftrans<-≤ lt (subst (λ k → k ≤ a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) )
            pcmp (ic-isup i i<x s<x fca) (ic-isup i i<y s<y fcb) refl = fcn-cmp _ f mf fca (subst (λ k → FClosure A f k b) pc01 fcb ) where
                pc01 : supfz i<y ≡ supfz i<x
-               pc01 = zeq ? ? ? ?
+               pc01 = cong supfz  o<-irr
+               -- zeq does not work here
       ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia)
 
 
@@ -1385,16 +1386,16 @@
                sa = ZChain.supf (pzc  (ob<x lim a<x)) a
                m =  omax a sa     -- x is limit ordinal, so we have sa o< m o< x
                m<x : m o< x
-               m<x with trio< a sa | inspect (omax a) sa
-               ... | tri< a<sa ¬b ¬c | record { eq = eq } = ob<x lim (ordtrans<-≤ sa<b b≤x )
-               ... | tri≈ ¬a a=sa ¬c | record { eq = eq } = subst (λ k → k o< x) eq zc41 where
+               m<x with trio< a sa 
+               ... | tri< a<sa ¬b ¬c = ob<x lim (ordtrans<-≤ sa<b b≤x )
+               ... | tri≈ ¬a a=sa ¬c = subst (λ k → k o< x) ? zc41 where
                    zc41 : omax a sa o< x
                    zc41 = osucprev ( begin
                        osuc ( omax a sa ) ≡⟨ cong (λ k → osuc (omax a k)) (sym a=sa) ⟩
                        osuc ( omax a a ) ≡⟨ cong osuc (omxx _) ⟩
                        osuc ( osuc  a ) ≤⟨ o<→≤ (ob<x lim (ob<x lim a<x))  ⟩
                        x ∎ ) where open o≤-Reasoning O
-               ... | tri> ¬a ¬b c | record { eq = eq } = ob<x lim a<x
+               ... | tri> ¬a ¬b c = ob<x lim a<x
                sam = ZChain.supf (pzc (ob<x lim m<x)) a
                zc42 : osuc a o≤ osuc m
                zc42 = osucc (o<→≤ ( omax-x _ _ ) )