⚠ 您正在浏览 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 壳及其塌缩
      • 从已计数的起点计数 Skolem 壳
      • 把无穷可构造层单射到其指标
      • 有界子集落在受控层
      • 可构造宇宙满足 GCH
module Cubical.Algebra.Monoid where

open import Cubical.Algebra.Monoid.Base public
使用改编自 1lab 的生成器渲染 (AGPL-3.0)。
llms.txt
© 2026 Bedrock Institute · 内容以 CC BY-NC-SA 4.0 许可 · 源码