2019-06-24 |
Shinji KONO |
HOD
|
2019-06-20 |
Shinji KONO |
...
|
2019-06-18 |
Shinji KONO |
dead end
|
2019-06-18 |
Shinji KONO |
remove o<→c< and add otrans in OD
|
2019-06-18 |
Shinji KONO |
dead end?
|
2019-06-16 |
Shinji KONO |
add assumption
|
2019-06-16 |
Shinji KONO |
add Ord Ordinal order preserving map
|
2019-06-16 |
Shinji KONO |
power set
|
2019-06-15 |
Shinji KONO |
...
|
2019-06-12 |
Shinji KONO |
starting over HOD
|
2019-06-10 |
Shinji KONO |
ZF Set Theory in Agda
release
|
2019-06-10 |
Shinji KONO |
Added tag current for changeset a402881cc341
|
2019-06-10 |
Shinji KONO |
add comment
|
2019-06-10 |
Shinji KONO |
Power Set done with min-sup assumption
|
2019-06-09 |
Shinji KONO |
...
|
2019-06-09 |
Shinji KONO |
power set using sup on Def
|
2019-06-08 |
Shinji KONO |
Power Set and L
|
2019-06-08 |
Shinji KONO |
clean up
|
2019-06-08 |
Shinji KONO |
...
|
2019-06-06 |
Shinji KONO |
replacement
|
2019-06-05 |
Shinji KONO |
Added tag current for changeset b4742cf4ef97
|
2019-06-05 |
Shinji KONO |
infinity axiom done
|
2019-06-05 |
Shinji KONO |
def ord conversion
|
2019-06-05 |
Shinji KONO |
...
|
2019-06-05 |
Shinji KONO |
osuc work around done
|
2019-06-04 |
Shinji KONO |
split omax?
|
2019-06-04 |
Shinji KONO |
internal error
|
2019-06-04 |
Shinji KONO |
omax-induction does not work
|
2019-06-04 |
Shinji KONO |
omax ..
|
2019-06-04 |
Shinji KONO |
...
|
2019-06-04 |
Shinji KONO |
Union (x , y) == (x , y ) only true on infinite case
|
2019-06-03 |
Shinji KONO |
simpler ordinal
|
2019-06-03 |
Shinji KONO |
remove ∅-base-def
|
2019-06-03 |
Shinji KONO |
add some lemma
|
2019-06-03 |
Shinji KONO |
infinite and replacement begin
|
2019-06-02 |
Shinji KONO |
Power Set on going ...
|
2019-06-02 |
Shinji KONO |
extensionality done
|
2019-06-02 |
Shinji KONO |
Union done
|
2019-06-01 |
Shinji KONO |
ordinal atomical successor?
|
2019-06-01 |
Shinji KONO |
fix ordinal
|
2019-06-01 |
Shinji KONO |
...
|
2019-06-01 |
Shinji KONO |
add osuc ( next larger element of Ordinal )
|
2019-06-01 |
Shinji KONO |
Union needs +1 space
|
2019-05-31 |
Shinji KONO |
union continue
|
2019-05-29 |
Shinji KONO |
Union
|
2019-05-29 |
Shinji KONO |
Added tag current for changeset 92a11dc6425c
|
2019-05-29 |
Shinji KONO |
regularity done
|
2019-05-29 |
Shinji KONO |
¬∅=→∅∈ : {n : Level} → { x : OD {suc n} } → ¬ ( x == od∅ {suc n} ) → x ∋ od∅ {suc n}
|
2019-05-29 |
Shinji KONO |
equal
|
2019-05-29 |
Shinji KONO |
omin
|
2019-05-29 |
Shinji KONO |
...
|
2019-05-29 |
Shinji KONO |
fix
|
2019-05-29 |
Shinji KONO |
dead end
|
2019-05-28 |
Shinji KONO |
lemma = cong₂ (λ x not → minimul x not ) oiso { }6
|
2019-05-28 |
Shinji KONO |
...
|
2019-05-28 |
Shinji KONO |
...
|
2019-05-27 |
Shinji KONO |
almost ...
|
2019-05-27 |
Shinji KONO |
regurality elimination case
|
2019-05-27 |
Shinji KONO |
fix selection axiom
|
2019-05-27 |
Shinji KONO |
...
|
2019-05-27 |
Shinji KONO |
tri-c<
|
2019-05-27 |
Shinji KONO |
...
|
2019-05-25 |
Shinji KONO |
...
|
2019-05-25 |
Shinji KONO |
fix Select
|
2019-05-25 |
Shinji KONO |
Added tag current for changeset 264784731a67
|
2019-05-25 |
Shinji KONO |
clean up
|
2019-05-25 |
Shinji KONO |
== and ∅7
|
2019-05-24 |
Shinji KONO |
od∅' {n} = ord→od (o∅ {n})
|
2019-05-24 |
Shinji KONO |
od→lv : {n : Level} → OD {n} → Nat
|
2019-05-24 |
Shinji KONO |
equalitu and internal parametorisity
|
2019-05-24 |
Shinji KONO |
regurality
|
2019-05-23 |
Shinji KONO |
mnimul
|
2019-05-23 |
Shinji KONO |
...
|
2019-05-23 |
Shinji KONO |
...
|
2019-05-23 |
Shinji KONO |
...
|
2019-05-23 |
Shinji KONO |
¬ ( y c< x ) → x ≡ od∅
|
2019-05-22 |
Shinji KONO |
transitive
|
2019-05-22 |
Shinji KONO |
ordinal fixed
|
2019-05-22 |
Shinji KONO |
fix oridinal
|
2019-05-21 |
Shinji KONO |
fix
|
2019-05-21 |
Shinji KONO |
oridnal dead end
|
2019-05-21 |
Shinji KONO |
fix ordinal
|
2019-05-20 |
Shinji KONO |
problem on Ordinal ( OSuc ℵ )
|
2019-05-20 |
Shinji KONO |
posturate OD is isomorphic to Ordinal
|
2019-05-19 |
Shinji KONO |
OD continue
|
2019-05-19 |
Shinji KONO |
OD, HOD, TC
|
2019-05-18 |
Shinji KONO |
dom-ψ
|
2019-05-18 |
Shinji KONO |
...
|
2019-05-18 |
Shinji KONO |
separte level
|
2019-05-17 |
Shinji KONO |
Sup
|
2019-05-16 |
Shinji KONO |
..
|
2019-05-16 |
Shinji KONO |
add transfinite
|
2019-05-16 |
Shinji KONO |
...
|
2019-05-16 |
Shinji KONO |
...
|
2019-05-16 |
Shinji KONO |
fix
|
2019-05-14 |
Shinji KONO |
clean up
|
2019-05-14 |
Shinji KONO |
...
|
2019-05-13 |
Shinji KONO |
fix
|
2019-05-13 |
Shinji KONO |
separete constructible set
|
2019-05-13 |
Shinji KONO |
dead end
|
2019-05-13 |
Shinji KONO |
dead end
|
2019-05-13 |
Shinji KONO |
...
|
2019-05-13 |
Shinji KONO |
add constructible set
|
2019-05-12 |
Shinji KONO |
try to fix axiom of replacement
|
2019-05-12 |
Shinji KONO |
fix
|
2019-05-11 |
Shinji KONO |
...
|
2019-05-11 |
Shinji KONO |
isEquiv and isZF
|
2019-05-11 |
Shinji KONO |
ZF in Agda
release
|
2019-05-11 |
Shinji KONO |
...
|
2019-05-11 |
Shinji KONO |
reocrd ZF
|
2019-05-08 |
Shinji KONO |
...
|
2019-05-08 |
Shinji KONO |
union
|
2019-05-08 |
Shinji KONO |
Set theory in Agda
|