log

age author description
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