⚠ Cubical ライブラリを閲覧しています。 Bedrock に戻る
Bedrock
English · 中文 · 日本語
このページの内容
メニュー
読書案内
  • 学習ルート
  • 依存マップ
  • マイルストーン
  • 用語集
モジュール
  • Base
    • 基礎語彙
    • 非可述性
    • 古典論理との境界
    • 選択原理
  • FOL
    • 対象言語
    • 構造
    • 意味論
    • Lévy 階層
    • 絶対性
    • ZF と ZFC のモデル
    • Manipulation
      • 定数の写像
      • 変数の改名
      • 定数の改名
      • 相対化
      • 定数の有界性
      • 出現ごとに扱う定数
      • パラメータ抽象
    • 集合としての構文
  • V
    • 累積階層
    • 累積階層における小さな真理値
    • 累積階層は ZF と ZFC のモデル
    • 累積階層の内部での符号化
    • 集合の小さな提示
    • 小さな提示に対する Cantor–Schröder–Bernstein の定理
    • Mostowski 崩壊
  • L
    • 集合の定義可能な部分集合
    • 構成可能階層と構成可能宇宙
    • 順序数の閉性と有限順序数
    • von Neumann ランク
    • Ordinal
      • 順序数は所属によって線形に順序付けられる
      • 構成可能階層の中で順序数を位置付ける
      • 順序数の添字、Gödel 対順序、有限添字
    • 最小の構成可能段階の添字
    • Axioms
      • 基本公理
      • 有界な分出公理と置換公理
      • 完全な分出公理と置換公理
      • L における冪集合
      • 数項列
      • L における無限公理
    • 存在論理式の構成可能段階への反映
    • 任意の論理式に対する反映
    • 周囲の論理式から L 上の論理式へ
    • Coding
      • 単集合と対を表す論理式
      • 集合で符号化した有限環境
      • 構成可能モデル上の論理式の符号化
      • 符号化再帰のための論理式表現
      • 部分符号に閉じた定義域
      • 符号化された対に沿う階数降下
      • 構成可能なコードと部分式の木
      • 部分式についての閉包
      • 固定長環境の集合
      • 論理式上の再帰による充足関係
      • 充足関係と再帰の値
      • 部分式上の充足関係表
      • 環境の集合の一致
      • コードスロットを七つの構成子について閉じる
      • 整形式な構成子キーの認識
      • コードから論理式を復元する
      • 後者演算について閉じた順序数段階の数項
      • 符号化された順序対の成分と有限論理式族を量化する
      • 環境の塔
      • すべての論理式の符号からなる集合
      • 閉じた論理式符号の定義域を記述する
      • 充足関係表を記述する
      • 論理式符号のアルファベット
      • 充足関係の節の読み取りと検証
      • 部分符号で閉じた領域上で再帰を固定する
      • 充足関係のグラフを表す論理式
      • 全コード上の一様な充足関係
      • 定義可能な冪集合を表す論理式
      • 構成可能階層を表す列
      • 符号化された単射
      • 一様な充足関係の内部グラフ
      • 閉じた符号の定義域の健全性と完全性
    • L における再帰的定義の内部化
    • Recursion
      • 再帰的定義のグラフ
    • L の内部における構成可能階層
    • Choice
      • 集合と交わる最初の段階
      • 有限段階上の整列順序
      • 後者段階の要素の正準な名前
      • 各段階上の整列順序
      • 名前の比較を表す論理式
      • 段階順序の内部の表
      • 段階順序の記述の妥当性
      • 名前の比較の妥当性
      • L の内部にある極限段階の順序
      • 最初の相違の関係からなる内部の族
      • 内部の段階順序関係
      • 横断集合による選択
    • WellOrder
      • 狭義整列順序と最小要素の探索
    • 構成可能宇宙は ZFC のモデル
    • L の内部における基数と符号化された単射
    • 定義可能な単射を内部コードにする
    • 符号化された単射の合成と包含
    • L の内部における一般連続体仮説
    • L の内部における Cantor–Schröder–Bernstein の定理
    • 推移的な整礎関係の崩壊
    • 任意の L 基数より大きい順序数 L 基数
    • GCH
      • 四つの内部上界から GCH を組み立てる
      • 充足関係表の Δ₀ 記述
      • 定義可能冪集合の Δ₀ 記述
      • GCH の議論に必要な十分な段階
      • 構成可能宇宙における ω 再帰
      • Skolem 包を構成して崩壊させる
      • 構成可能階層の Δ₀ 記述
      • 凝縮を通して構造を移す
      • 後続基数より小さい順序数をその基数へ単射する
      • L の内部で順序型を構成する
      • 順序数の基数代表を選ぶ
      • L の無限基数における平方律
      • 構成可能な段階における最小の証人の写像
      • 後続基数を冪集合へ単射する
      • 無限順序数の下で有限列をコード化する
      • 無限な構成可能段階を数える道具
      • 包とその崩壊を L の内部に置く
      • 数えられた始集合から Skolem 包を数える
      • 無限構成可能段階をその添字へ単射する
      • 有界部分集合が制御された段階に現れる
      • 構成可能宇宙は GCH を満たす
module Cubical.Data.Sum where

open import Cubical.Data.Sum.Base public
open import Cubical.Data.Sum.Properties public
1lab を改変したジェネレータでレンダリング (AGPL-3.0)。
llms.txt
© 2026 Bedrock Institute · コンテンツは CC BY-NC-SA 4.0 ライセンス · ソース