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

comparison Ordinals.agda @ 326:feeba7fd499a

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 Sun, 05 Jul 2020 03:45:41 +0900
parents fbabb20f222e
children 5544f4921a44
comparison
equal deleted inserted replaced
325:1a54dbe1ea4c 326:feeba7fd499a
109 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy 109 proj1 (osuc2 x y) ox<ooy with osuc-≡< ox<ooy
110 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy 110 proj1 (osuc2 x y) ox<ooy | case1 ox=oy = o<-subst <-osuc refl ox=oy
111 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 111 proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy
112 112
113 _o≤_ : Ordinal → Ordinal → Set n 113 _o≤_ : Ordinal → Ordinal → Set n
114 a o≤ b = (a ≡ b) ∨ ( a o< b ) 114 a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b )
115 115
116 116
117 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob 117 xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob
118 xo<ab {oa} {ob} a→b with trio< oa ob 118 xo<ab {oa} {ob} a→b with trio< oa ob
119 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc 119 xo<ab {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
181 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x) 181 omxxx : ( x : Ordinal ) → omax x (omax x x ) ≡ osuc (osuc x)
182 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc )) 182 omxxx x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
183 183
184 open _∧_ 184 open _∧_
185 185
186 o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j
187 o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
186 OrdTrans : Transitive _o≤_ 188 OrdTrans : Transitive _o≤_
187 OrdTrans (case1 refl) (case1 refl) = case1 refl 189 OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
188 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 190 OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
189 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 191 OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
190 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) 192 OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
193 OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc
191 194
192 OrdPreorder : Preorder n n n 195 OrdPreorder : Preorder n n n
193 OrdPreorder = record { Carrier = Ordinal 196 OrdPreorder = record { Carrier = Ordinal
194 ; _≈_ = _≡_ 197 ; _≈_ = _≡_
195 ; _∼_ = _o≤_ 198 ; _∼_ = _o≤_
196 ; isPreorder = record { 199 ; isPreorder = record {
197 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 200 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
198 ; reflexive = case1 201 ; reflexive = o≤-refl
199 ; trans = OrdTrans 202 ; trans = OrdTrans
200 } 203 }
201 } 204 }
202 205
203 FExists : {m l : Level} → ( ψ : Ordinal → Set m ) 206 FExists : {m l : Level} → ( ψ : Ordinal → Set m )