Mathstodon

0 posts0 participants0 posts today

Hexirp PrixehAczel's encoding は、 Set = Σ [X : Type] [X → Set] というようになる帰納型を使い型理論で集合を符号化するという方法なんだけど、ここの X → Set は重複が許されるので実際は多重集合である。この写像を単射だけに限ることで集合にすることが出来て、そうすると更に色々と都合が良い性質を得られるらしい。 <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a> RE: <a href="https://mathstodon.xyz/users/mortberg/statuses/111940426219409755" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/mortberg/statuses/111940426219409755</a>

Hexirp Prixehequivalence を弱めた関係を複数定義し、それらの関係を考察し、それにより equivalence ではない場合についても書き換えができるような Coq のプラグインを実装している。 <a href="https://misskey.io/tags/Coq" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a href="https://misskey.io/tags/HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a> RE: <a href="https://mathstodon.xyz/users/Jose_A_Alonso/statuses/111968275067608880" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/Jose_A_Alonso/statuses/111968275067608880</a>

Hexirp PrixehIngo Blechschmidt - Towards multiversal modal operators for homotopy type theory - <a href="https://youtu.be/L6dKpt7UqX4" rel="nofollow noopener noreferrer" target="_blank">https://youtu.be/L6dKpt7UqX4</a> Hamkins は 2011 年に多元宇宙主義を提唱している。 Joel David Hamkins - The set-theoretic multiverse - <a href="https://arxiv.org/abs/1108.4223" rel="nofollow noopener noreferrer" target="_blank">https://arxiv.org/abs/1108.4223</a> 連続体仮説は ZFC の宇宙で成り立ったり成り立たなかったりする。 ZFC の宇宙は様々な種類があり、それらは枝分かれしながら拡張していく。そこで、これらの様々な宇宙を全て考慮する次のような演算子を導入する。 * "◇ T" - 今いる宇宙を拡張した宇宙のうちに T が成立するような宇宙が存在する。 * "□ T" - 今いる宇宙を拡張した全ての宇宙で T が成立する。 □ ( ◇ CH ∧ ◇ ( ￢ CH ) ) は、どのような拡張においても、連続体仮説が成り立つように拡張することも連続体仮説が成り立たないように拡張することも常に出来る、ということを表す。 この多元宇宙主義を Homotopy Type Theory にも適用しようぜ、という感じの発表っぽい？ <a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a> <a href="https://misskey.io/tags/様相論理" rel="nofollow noopener noreferrer" target="_blank">#様相論理</a> <a href="https://misskey.io/tags/様相演算子" rel="nofollow noopener noreferrer" target="_blank">#様相演算子</a>

Hexirp Prixeh<a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/HoTT" rel="nofollow noopener noreferrer" target="_blank">#HoTT</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a> RE: <a href="https://mathstodon.xyz/users/de_Jong_Tom/statuses/111499525477681029" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/de_Jong_Tom/statuses/111499525477681029</a>

Hexirp Prixeh<a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/プログラミング" rel="nofollow noopener noreferrer" target="_blank">#プログラミング</a> <a href="https://misskey.io/tags/トポロジー" rel="nofollow noopener noreferrer" target="_blank">#トポロジー</a> <a href="https://misskey.io/tags/計算可能実数" rel="nofollow noopener noreferrer" target="_blank">#計算可能実数</a> <a href="https://misskey.io/tags/計算可能性理論" rel="nofollow noopener noreferrer" target="_blank">#計算可能性理論</a> <a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> RE: <a href="https://mathstodon.xyz/users/MartinEscardo/statuses/111439342950964225" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/MartinEscardo/statuses/111439342950964225</a>

Hexirp Prixeh位相空間におけるチコノフの定理には選択公理が必要だけど、 locale におけるチコノフの定理は構成的に証明できる <a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a>

Hexirp Prixeh構成主義者としては位相空間ではなく locale を使いたい <a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a>

Hexirp PrixehPeter Aczel が死去したとのことである。 型理論の中で集合論を実装する際に使える Peter Aczel's encoding というものがある。次のような定義である。 <pre><code>Inductive V@{ i j | i < j } : Type@{j} := set : forall A : Type@{i}, (A -> V) -> V.</code></pre> coq-contribs/zfc - <a href="https://github.com/coq-contribs/zfc" rel="nofollow noopener noreferrer" target="_blank">https://github.com/coq-contribs/zfc</a> このエンコーディングと幾つかの公理を用いて Coq の中で ZFC のモデルを作るライブラリが coq-contribs/zfc である。 Homotopy Type Theory: Univalent Foundations of Mathematics - <a href="https://arxiv.org/abs/1308.0729" rel="nofollow noopener noreferrer" target="_blank">https://arxiv.org/abs/1308.0729</a> HoTT Book の Definition 10.5.1 において ZFC のモデルとなる型を定義する際にも higher inductive types を使った Peter Aczel's encoding の変種が使われている。 R.I.P. <a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/集合論" rel="nofollow noopener noreferrer" target="_blank">#集合論</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> RE: <a href="https://bi.cbult.space/objects/0b3c798f-5dce-46d4-988b-8c349da45344" rel="nofollow noopener noreferrer" target="_blank">https://bi.cbult.space/objects/0b3c798f-5dce-46d4-988b-8c349da45344</a>

Hexirp Prixeh整礎な木 (W-types) の深さを測ることについて。 その深さは有限ではなければならない。しかし、その深さを単純に自然数型で測ろうとすると「型が空であるため子を持たない」と「型が空ではないため子を持つ」の場合分けが必要となって構成的ではなくなる。そのため、自然数型の変種を定義して、それで深さを測り、それが有限であることが証明する。 <a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> RE: <a href="https://mathstodon.xyz/users/MartinEscardo/statuses/110764915123711649" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/MartinEscardo/statuses/110764915123711649</a>

Hexirp Prixeh<a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/集合論" rel="nofollow noopener noreferrer" target="_blank">#集合論</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> RE: <a href="https://mathstodon.xyz/users/MartinEscardo/statuses/110567061223508698" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/MartinEscardo/statuses/110567061223508698</a>

Hexirp Prixeh<a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/直観主義論理" rel="nofollow noopener noreferrer" target="_blank">#直観主義論理</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> RE: <a href="https://mathstodon.xyz/users/MartinEscardo/statuses/110549967500023998" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/MartinEscardo/statuses/110549967500023998</a>

Hexirp Prixeh<a href="https://misskey.io/tags/数学" rel="nofollow noopener noreferrer" target="_blank">#数学</a> <a href="https://misskey.io/tags/型理論" rel="nofollow noopener noreferrer" target="_blank">#型理論</a> <a href="https://misskey.io/tags/定理証明支援系" rel="nofollow noopener noreferrer" target="_blank">#定理証明支援系</a> <a href="https://misskey.io/tags/Agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a href="https://misskey.io/tags/構成主義数学" rel="nofollow noopener noreferrer" target="_blank">#構成主義数学</a> RE: <a href="https://mathstodon.xyz/users/MartinEscardo/statuses/110504563233350460" rel="nofollow noopener noreferrer" target="_blank">https://mathstodon.xyz/users/MartinEscardo/statuses/110504563233350460</a>

Recent searches

Search options

Administered by:

Server stats:

#構成主義数学