| 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
|
