Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff Ordinals.agda @ 326:feeba7fd499a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Jul 2020 03:45:41 +0900 |
| parents | fbabb20f222e |
| children | 5544f4921a44 |
line wrap: on
line diff
--- a/Ordinals.agda Sat Jul 04 22:48:49 2020 +0900 +++ b/Ordinals.agda Sun Jul 05 03:45:41 2020 +0900 @@ -111,7 +111,7 @@ proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy _o≤_ : Ordinal → Ordinal → Set n - a o≤ b = (a ≡ b) ∨ ( a o< b ) + a o≤ b = a o< osuc b -- (a ≡ b) ∨ ( a o< b ) xo<ab : {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa → ox o< ob ) → oa o< osuc ob @@ -183,11 +183,14 @@ open _∧_ + o≤-refl : { i j : Ordinal } → i ≡ j → i o≤ j + o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc OrdTrans : Transitive _o≤_ - OrdTrans (case1 refl) (case1 refl) = case1 refl - OrdTrans (case1 refl) (case2 lt2) = case2 lt2 - OrdTrans (case2 lt1) (case1 refl) = case2 lt1 - OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y) + OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c + OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc + OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc + OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc + OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b b<c) <-osuc OrdPreorder : Preorder n n n OrdPreorder = record { Carrier = Ordinal @@ -195,7 +198,7 @@ ; _∼_ = _o≤_ ; isPreorder = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans } - ; reflexive = case1 + ; reflexive = o≤-refl ; trans = OrdTrans } }