Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 917:4d99a1306f40
roll back
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Oct 2022 19:54:20 +0900 |
| parents | f0b98f57ec65 |
| children | |
| files | src/zorn.agda |
| diffstat | 1 files changed, 57 insertions(+), 73 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Oct 13 17:47:19 2022 +0900 +++ b/src/zorn.agda Sat Oct 15 19:54:20 2022 +0900 @@ -407,7 +407,7 @@ minsup : {x : Ordinal } → x o≤ z → MinSUP A (UnionCF A f mf ay supf x) supf-is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ MinSUP.sup ( minsup x≤z ) - csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain + csupf : {b : Ordinal } → b o< z → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) -- supf z is not an element of this chain chain : HOD chain = UnionCF A f mf ay supf z @@ -601,14 +601,14 @@ supf = ZChain.supf zc - csupf-fc : {b s z1 : Ordinal} → b o≤ & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 - csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where + csupf-fc : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → UnionCF A f mf ay supf b ∋ * z1 + csupf-fc {b} {s} {z1} b<z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where s<b : s o< b s<b = ZChain.supf-inject zc ss<sb - s≤<z : s o≤ & A - s≤<z = ordtrans s<b b≤z + s<z : s o< & A + s<z = ordtrans s<b b<z zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s) - zc04 = ZChain.csupf zc (z09 (ZChain.asupf zc)) + zc04 = ZChain.csupf zc s<z (z09 (ZChain.asupf zc)) zc05 : odef (UnionCF A f mf ay supf b) (supf s) zc05 with zc04 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ @@ -624,10 +624,11 @@ zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) order {b} {s} {z1} b<z ss<sb fc = zc04 where zc00 : ( z1 ≡ MinSUP.sup (ZChain.minsup zc (o<→≤ b<z) )) ∨ ( z1 << MinSUP.sup ( ZChain.minsup zc (o<→≤ b<z) ) ) - zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc (o<→≤ b<z) ss<sb fc )) + zc00 = MinSUP.x<sup (ZChain.minsup zc (o<→≤ b<z) ) (subst (λ k → odef (UnionCF A f mf ay (ZChain.supf zc) b) k ) &iso (csupf-fc b<z ss<sb fc )) -- supf (supf b) ≡ supf b zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) zc04 with zc00 @@ -796,8 +797,10 @@ zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) px<x : px o< x px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc + opx=x : osuc px ≡ x + opx=x = Oprev.oprev=x op zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px - zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt + zc-b<x b lt = subst (λ k → b o< k ) (sym opx=x) lt supf0 = ZChain.supf zc pchain : HOD @@ -812,7 +815,7 @@ ... | tri≈ ¬a b ¬c = case1 (o≤-refl0 b) ... | tri> ¬a ¬b px<b with osuc-≡< b≤x ... | case1 eq = case2 eq - ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) + ... | case2 b<x = ⊥-elim ( ¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym opx=x) b<x ⟫ ) zc41 : supf0 px o< x → ZChain A f mf ay x zc41 sfpx<x = record { supf = supf1 ; sup=u = ? ; asupf = ? ; supf-mono = supf1-mono ; supf-< = ? @@ -945,7 +948,7 @@ zc13 : {z : Ordinal } → FClosure A f y z → (z ≡ supf0 u) ∨ ( z << supf0 u ) zc13 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sf1=sf0 (o<→≤ a)) ( ChainP.fcy<sup is-sup fc ) ... | tri≈ ¬a b ¬c | _ = case2 (init (subst (λ k → odef A k) (cong supf0 b) asp ) (cong supf0 (sym b)) ) - ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op)) u<x ⟫ ) + ... | tri> ¬a ¬b c | _ = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym opx=x) u<x ⟫ ) zc12 : {z : Ordinal} → odef pchainpx z → odef (UnionCF A f mf ay supf1 x) z zc12 {z} (case1 ⟪ az , ch-init fc ⟫ ) = ⟪ az , ch-init fc ⟫ zc12 {z} (case1 ⟪ az , ch-is-sup u u<x is-sup fc ⟫ ) = zc21 fc where @@ -955,7 +958,7 @@ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ zc21 (init asp refl ) with trio< u px | inspect supf1 u ... | tri< a ¬b ¬c | _ = ⟪ asp , ch-is-sup u - (subst (λ k → u o< k) (Oprev.oprev=x op) (ordtrans u<x <-osuc)) + (subst (λ k → u o< k) opx=x (ordtrans u<x <-osuc)) record {fcy<sup = zc13 ; order = zc17 ; supu=u = trans (sf1=sf0 (o<→≤ u<x)) (ChainP.supu=u is-sup) } zc14 ⟫ where zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 u → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 u) ∨ (z1 << supf1 u) @@ -992,7 +995,7 @@ zc21 {z1} (fsuc z2 fc ) with zc21 fc ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x u1-is-sup (fsuc _ fc₁) ⟫ - zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x ) + zc21 (init asp refl ) with osuc-≡< ( subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x ) ... | case1 sfpx=px = ⟪ asp , ch-is-sup px (pxo<x op) record {fcy<sup = zc13 ; order = zc17 ; supu=u = zc15 } zc14 ⟫ where zc15 : supf1 px ≡ px @@ -1004,7 +1007,7 @@ zc17 : {s : Ordinal} {z1 : Ordinal} → supf1 s o< supf1 px → FClosure A f (supf1 s) z1 → (z1 ≡ supf1 px) ∨ (z1 << supf1 px) zc17 {s} {z1} ss<spx fc = subst (λ k → (z1 ≡ k) ∨ (z1 << k )) mins-is-spx - (MinSUP.x<sup mins (csupf17 (fcup fc (o<→≤ s<px) )) ) where + (MinSUP.x<sup mins (zc18 (fcup fc (o<→≤ s<px) )) ) where mins : MinSUP A (UnionCF A f mf ay supf0 px) mins = ZChain.minsup zc o≤-refl mins-is-spx : MinSUP.sup mins ≡ supf1 px @@ -1013,28 +1016,35 @@ s<px = supf-inject0 supf1-mono ss<spx sf<px : supf0 s o< px sf<px = subst₂ (λ j k → j o< k ) (sf1=sf0 (o<→≤ s<px)) (trans (sf1=sf0 o≤-refl) (sfpx=px)) ss<spx - csupf17 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 - csupf17 (init as refl ) = ZChain.csupf zc sf<px - csupf17 (fsuc x fc) = ZChain.f-next zc (csupf17 fc) - - ... | case2 sfp<px with ZChain.csupf zc sfp<px -- odef (UnionCF A f mf ay supf0 px) (supf0 px) - ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ ua1 , ch-init fc₁ ⟫ - ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ ua1 , ch-is-sup u (ordtrans u≤x px<x) - record { fcy<sup = z10 ; order = z11 ; supu=u = z12 } (fcpu fc₁ (o<→≤ u≤x) ) ⟫ where - z10 : {z : Ordinal } → FClosure A f y z → (z ≡ supf1 u) ∨ ( z << supf1 u ) - z10 {z} fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) (ChainP.fcy<sup is-sup fc) - z11 : {s z1 : Ordinal} → (lt : supf1 s o< supf1 u ) → FClosure A f (supf1 s ) z1 - → (z1 ≡ supf1 u ) ∨ ( z1 << supf1 u ) - z11 {s} {z} lt fc = subst (λ k → (z ≡ k) ∨ ( z << k )) (sym (sf1=sf0 (o<→≤ u≤x))) - (ChainP.order is-sup lt0 (fcup fc s≤px )) where - s<u : s o< u - s<u = supf-inject0 supf1-mono lt - s≤px : s o≤ px - s≤px = ordtrans s<u (o<→≤ u≤x) - lt0 : supf0 s o< supf0 u - lt0 = subst₂ (λ j k → j o< k ) (sf1=sf0 s≤px) (sf1=sf0 (o<→≤ u≤x)) lt - z12 : supf1 u ≡ u - z12 = trans (sf1=sf0 (o<→≤ u≤x)) (ChainP.supu=u is-sup) + zc18 : {z1 : Ordinal } → FClosure A f (supf0 s) z1 → odef (UnionCF A f mf ay supf0 px) z1 + zc18 (init as refl ) = ZChain.csupf zc s<px sf<px + zc18 (fsuc x fc) = ZChain.f-next zc (zc18 fc) + ... | case2 sfpx<px = ⟪ ZChain.asupf zc , ch-is-sup (supf1 px) (subst (λ k → k o< x) (sym (sf1=sf0 o≤-refl)) sfpx<x ) + record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u (sf1=sf0 o≤-refl)) ) ⟫ where + minsfpx : MinSUP A (UnionCF A f mf ay supf0 (supf1 px)) + minsfpx = ZChain.minsup zc (o<→≤ (subst (λ k → k o< px) (sym (sf1=sf0 o≤-refl)) sfpx<px)) + mins : MinSUP A (UnionCF A f mf ay supf0 px) + mins = ZChain.minsup zc o≤-refl + mins-is-spx : MinSUP.sup mins ≡ supf1 px + mins-is-spx = trans (sym ( ZChain.supf-is-minsup zc o≤-refl ) ) (sym (sf1=sf0 o≤-refl )) + supu=u : supf1 (supf1 px) ≡ supf1 px + supu=u with osuc-≡< (supf1-mono (o<→≤ sfpx<px)) + ... | case1 eq = trans (cong supf1 (sf1=sf0 o≤-refl) ) eq + ... | case2 ss<sfpx = ? where + zc30 : supf1 px o< px + zc30 = subst (λ k → k o< px) (sym (sf1=sf0 o≤-refl )) sfpx<px + zc32 : supf1 (supf0 px) ≡ supf0 (supf1 px) + zc32 = trans (sf1=sf0 (subst (λ k → supf0 px o< k) (sym opx=x) sfpx<x) ) + ( cong supf0 (sym (sf1=sf0 o≤-refl ) ) ) + zc31 : supf0 (supf1 px) o< px + zc31 = subst (λ k → k o< px ) zc32 ( ordtrans ss<sfpx (subst (λ k → k o< px ) + (sym (sf1=sf0 o≤-refl )) sfpx<px )) + cs05 : odef (UnionCF A f mf ay supf0 px) (supf0 (supf1 px)) + cs05 = ZChain.csupf zc zc30 zc31 + cs06 : supf1 (supf1 px) ≡ supf1 px + cs06 with cs05 + ... | ⟪ ua1 , ch-init fc ⟫ = ? + ... | ⟪ ua1 , ch-is-sup u u≤x u1-is-sup fcp ⟫ = ? @@ -1070,21 +1080,19 @@ odef (UnionCF A f mf ay supf1 z) x → (x ≡ sup2) ∨ (x << sup2)) → MinSUP.sup m o≤ sup2 ms01 {sup2} us P = MinSUP.minsup m ? ? - csupf1 : {z1 : Ordinal } → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) - csupf1 {z1} sz1<x = csupf2 where + csupf1 : {z1 : Ordinal } → z1 o< x → supf1 z1 o< x → odef (UnionCF A f mf ay supf1 x) (supf1 z1) + csupf1 {z1} z1<x sz1<x = csupf2 where -- z1 o< px → supf1 z1 ≡ supf0 z1 -- z1 ≡ px , supf0 px o< px .. px o< z1, x o≤ z1 ... supf1 z1 ≡ sp1 -- z1 ≡ px , supf0 px ≡ px psz1≤px : supf1 z1 o≤ px - psz1≤px = subst (λ k → supf1 z1 o< k ) (sym (Oprev.oprev=x op)) sz1<x - cs01 : supf0 px o< px → odef (UnionCF A f mf ay supf0 px) (supf0 px) - cs01 spx<px = ZChain.csupf zc spx<px + psz1≤px = subst (λ k → supf1 z1 o< k ) (sym opx=x) sz1<x csupf2 : odef (UnionCF A f mf ay supf1 x) (supf1 z1) csupf2 with trio< z1 px | inspect supf1 z1 csupf2 | tri< a ¬b ¬c | record { eq = eq1 } with osuc-≡< psz1≤px ... | case2 lt = zc12 (case1 cs03) where cs03 : odef (UnionCF A f mf ay supf0 px) (supf0 z1) - cs03 = ZChain.csupf zc (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) + cs03 = ZChain.csupf zc a (subst (λ k → k o< px) (sf1=sf0 (o<→≤ a)) lt ) ... | case1 sfz=px with osuc-≡< ( supf1-mono (o<→≤ a) ) ... | case1 sfz=sfpx = zc12 (case2 (init (ZChain.asupf zc) cs04 )) where supu=u : supf1 (supf1 z1) ≡ supf1 z1 @@ -1100,33 +1108,9 @@ cs05 : px o< supf0 px cs05 = subst₂ ( λ j k → j o< k ) sfz=px (sf1=sf0 o≤-refl ) sfz<sfpx cs06 : supf0 px o< osuc px - cs06 = subst (λ k → supf0 px o< k ) (sym (Oprev.oprev=x op)) sfpx<x + cs06 = subst (λ k → supf0 px o< k ) (sym opx=x) sfpx<x csupf2 | tri≈ ¬a b ¬c | record { eq = eq1 } = zc12 (case2 (init (ZChain.asupf zc) (cong supf0 (sym b)))) - csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } - = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) - record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - supu=u : supf1 (supf1 z1) ≡ supf1 z1 - supu=u = ? - sp1≤px : sp1 o≤ px - sp1≤px with trio< sp1 px - ... | tri< a ¬b ¬c = o<→≤ a - ... | tri≈ ¬a b ¬c = o≤-refl0 b - ... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) - - -- with trio< sp1 px - -- ... | tri< sp1<px ¬b ¬c = ? -- supf1 z1 = sp1 o< px o< z1 - -- ... | tri≈ ¬a sp1=px ¬c = ⟪ MinSUP.asm sup1 , ch-is-sup (supf1 z1) (subst (λ k → k o< x) (sym eq1) sz1<x) - -- record { fcy<sup = ? ; order = ? ; supu=u = supu=u } (init asupf1 (trans supu=u eq1) ) ⟫ where - -- -- supf1 z1 ≡ sp1, px o< z1, sp1 o< x -- sp1 o< z1 - -- -- supf1 sp1 o≤ supf1 z1 ≡ sp1 o< z1 - -- asm : odef A (supf1 z1) - -- asm = subst (λ k → odef A k ) (sym (sf1=sp1 px<z1)) ( MinSUP.asm sup1) - -- cs05 : odef (UnionCF A f mf ay supf1 x) (supf1 sp1) - -- cs05 = zc12 (case2 (init (ZChain.asupf zc) ( begin - -- supf0 px ≡⟨ sym (sf1=sf0 o≤-refl ) ⟩ - -- supf1 px ≡⟨ cong supf1 (sym sp1=px) ⟩ - -- supf1 sp1 ∎ ))) where open ≡-Reasoning - --... | tri> ¬a ¬b px<sp1 = ⊥-elim (¬p<x<op ⟪ px<sp1 , subst (λ k → sp1 o< k) (sym (Oprev.oprev=x op)) sz1<x ⟫ ) + csupf2 | tri> ¬a ¬b px<z1 | record { eq = eq1 } = ⊥-elim ( ¬p<x<op ⟪ px<z1 , subst (λ k → z1 o< k) (sym opx=x) z1<x ⟫ ) zc4 : ZChain A f mf ay x --- x o≤ supf px zc4 with trio< x (supf0 px) @@ -1189,13 +1173,13 @@ zc11 (case1 ¬sp=x) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = ⊥-elim (¬sp=x zcsup) where eq : u1 ≡ x eq with trio< u1 x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) + ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym opx=x) a ⟫ ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? ) s1u=x : supf0 u1 ≡ x s1u=x = trans ? eq zc13 : osuc px o< osuc u1 - zc13 = o≤-refl0 ( trans (Oprev.oprev=x op) (sym eq ) ) + zc13 = o≤-refl0 ( trans opx=x (sym eq ) ) x<sup : {w : Ordinal} → odef (UnionCF A f mf ay supf0 px) w → (w ≡ x) ∨ (w << x) x<sup {w} ⟪ az , ch-init {w} fc ⟫ = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? x<sup {w} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ with osuc-≡< ( supf-mono (ordtrans (o<→≤ u≤x) ? )) @@ -1205,7 +1189,7 @@ u ≡⟨ sym ( ChainP.supu=u is-sup) ⟩ supf0 u ≡⟨ ? ⟩ supf0 u1 ≡⟨ s1u=x ⟩ - x ≡⟨ sym (Oprev.oprev=x op) ⟩ + x ≡⟨ sym opx=x ⟩ osuc px ∎ where open ≡-Reasoning ... | case2 lt = subst (λ k → (w ≡ k) ∨ (w << k)) s1u=x ? zc12 : supf0 x ≡ u1 @@ -1216,7 +1200,7 @@ zc11 (case2 hp) {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ | tri> ¬a ¬b px<u = case1 ? where eq : u1 ≡ x eq with trio< u1 x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym (Oprev.oprev=x op )) a ⟫ ) + ... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<u , subst (λ k → u1 o< k ) (sym opx=x) a ⟫ ) ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c = ⊥-elim ( o<> u1<x ? ) zc20 : {z : Ordinal} → FClosure A f (supf0 u1) z → OD.def (od pchain) z @@ -1244,7 +1228,7 @@ zc30 : z ≡ x zc30 with osuc-≡< z≤x ... | case1 eq = eq - ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym (Oprev.oprev=x op)) z<x ⟫ ) + ... | case2 z<x = ⊥-elim (¬p<x<op ⟪ px<z , subst (λ k → z o< k ) (sym opx=x) z<x ⟫ ) zc32 = ZChain.sup zc o≤-refl zc34 : ¬ (supf0 px ≡ px) → {w : HOD} → UnionCF A f mf ay supf0 z ∋ w → (w ≡ SUP.sup zc32) ∨ (w < SUP.sup zc32) zc34 ne {w} lt with zc11 ? ⟪ proj1 lt , ? ⟫ @@ -1270,7 +1254,7 @@ zc30 : x ≡ b zc30 with osuc-≡< b≤x ... | case1 eq = sym (eq) - ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) b<x ⟫ ) + ... | case2 b<x = ⊥-elim (¬p<x<op ⟪ px<b , subst (λ k → b o< k ) (sym opx=x) b<x ⟫ ) zcsup : xSUP (UnionCF A f mf ay supf0 px) x zcsup with zc30 ... | refl = record { ax = ab ; is-sup = record { x<sup = λ {w} lt →