Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 502:3c03f5bf9e16

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 12 Apr 2022 15:58:53 +0900
parents 5a166a832472
children 1546541ed461
files src/zorn.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Apr 12 15:45:56 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 15:58:53 2022 +0900
@@ -138,7 +138,7 @@
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) cy)
       
-record IsIFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
+record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
    field
       icy : odef (IChainSet {A} (me ax)) y  
       c-finite : ¬ OSup> (IChainSet {A} (me ax)) (d→∋ (IChainSet {A} (me ax)) icy)
@@ -152,7 +152,7 @@
     Gtx = record { od = record { def = λ y → odef ( IChainSet x ) y ∧  ( & (elm x) o< y ) } ; odmax = & A
         ; <odmax = λ lt → subst (λ k → k o< & A) &iso (c<→o< (d→∋  A (proj1 (proj1 lt))))  }
     HG : HOD
-    HG = record { od = record { def = λ y → odef A y ∧ IsIFC A (d→∋ A (is-elm x) ) y } ; odmax = & A
+    HG = record { od = record { def = λ y → odef A y ∧ IsFC A (d→∋ A (is-elm x) ) y } ; odmax = & A
         ; <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)