用户贡献
- 2023 年 5 月 29 日 (一) 09:50 差异 历史 +1 m 有效意象 统一翻译 当前
- 2023 年 5 月 28 日 (日) 03:00 差异 历史 +7 m Brunerie 数 Fix link 当前
- 2023 年 5 月 27 日 (六) 03:39 差异 历史 +533 N 全忠实函子 创建页面，并添加内容 “\textbf{全忠实函子}指既是全函子又是忠实函子的函子, 是集合间单射概念在范畴论中的推广. == 定义 == \begin{def…”
- 2023 年 5 月 27 日 (六) 03:34 差异 历史 +29 N 全忠实 重定向页面至全忠实函子 当前 标签：新重定向
- 2023 年 5 月 26 日 (五) 23:01 差异 历史 +526 m Brunerie 数 定义映射
- 2023 年 5 月 25 日 (四) 23:15 差异 历史 +102 m 高阶归纳类型 trans 当前
- 2023 年 5 月 25 日 (四) 23:15 差异 历史 +306 m 高阶归纳类型 移除至高阶归纳类型 (同伦类型论)的重定向 标签：移除重定向
- 2023 年 5 月 25 日 (四) 23:12 差异 历史 +24 m 高阶归纳类型 (同伦类型论) 广义的高阶归纳类型 当前
- 2023 年 5 月 25 日 (四) 23:10 差异 历史 +51 N 高阶归纳类型 Ice1000移动页面高阶归纳类型至高阶归纳类型 (同伦类型论) 标签：新重定向
- 2023 年 5 月 25 日 (四) 23:10 差异 历史 0 m 高阶归纳类型 (同伦类型论) Ice1000移动页面高阶归纳类型至高阶归纳类型 (同伦类型论)
- 2023 年 5 月 25 日 (四) 21:49 差异 历史 +14 m Brunerie 数 修复事实错误
- 2023 年 5 月 25 日 (四) 12:14 差异 历史 +21 m 非直谓性 (类型论) 修复 当前
- 2023 年 5 月 25 日 (四) 11:41 差异 历史 +169 m 用户:Ice1000 new 当前
- 2023 年 5 月 24 日 (三) 14:11 差异 历史 +155 m 用户:Ice1000/神谕模态 加一些 remark
- 2023 年 5 月 24 日 (三) 14:08 差异 历史 +2,220 N 用户:Ice1000/缩积操作的五边形公理 创建页面，并添加内容 “== 动机 == 缩积操作是 $1$-融贯|范畴的, 换言之就是它满足五边形公理. 这个性质很有用, 在Brunerie 数…” 当前
- 2023 年 5 月 24 日 (三) 13:47 差异 历史 +921 N Brunerie 数 创建页面，并添加内容 “\textbf{Brunerie 数}是 $π_4(\mathbb S^3)=\mathbb Z/n\mathbb Z$ 中 $n$ 的解, 在经典同伦论中已经知道是 $\pm 2$, 但由 Guillaume Bruneri…”
- 2023 年 5 月 24 日 (三) 13:33 差异 历史 +26 N 缩积 重定向页面至缩积空间 当前 标签：新重定向
- 2023 年 5 月 24 日 (三) 13:33 差异 历史 +41 m 用户:Ice1000 加一个, 今天的其它的实在听不懂了
- 2023 年 5 月 24 日 (三) 13:28 差异 历史 +2,295 N 用户:Ice1000/神谕模态 创建页面，并添加内容 “考虑Gödel 编码的那一套理论 (见Kleene 第一代数) 里面的 $\varphi_e$, 记 $2$ 为两个元素的集合. == 基本定义 == \begin{d…”
- 2023 年 5 月 24 日 (三) 10:17 差异 历史 +36 N 自然数类型 Ice1000移动页面自然数类型至自然数 (类型论) 当前 标签：新重定向
- 2023 年 5 月 24 日 (三) 10:17 差异 历史 0 m 自然数 (类型论) Ice1000移动页面自然数类型至自然数 (类型论) 当前
- 2023 年 5 月 24 日 (三) 10:17 差异 历史 +36 N 无交并类型 Ice1000移动页面无交并类型至无交并 (类型论) 当前 标签：新重定向
- 2023 年 5 月 24 日 (三) 10:17 差异 历史 0 m 无交并 (类型论) Ice1000移动页面无交并类型至无交并 (类型论) 当前
- 2023 年 5 月 24 日 (三) 10:16 差异 历史 +30 N 积类型 Ice1000移动页面积类型至积 (类型论) 当前 标签：新重定向
- 2023 年 5 月 24 日 (三) 10:16 差异 历史 0 m 积 (类型论) Ice1000移动页面积类型至积 (类型论) 当前
- 2023 年 5 月 24 日 (三) 10:15 差异 历史 +33 N 函数类型 Ice1000移动页面函数类型至函数 (类型论) 当前 标签：新重定向
- 2023 年 5 月 24 日 (三) 10:15 差异 历史 0 m 函数 (类型论) Ice1000移动页面函数类型至函数 (类型论) 当前
- 2023 年 5 月 24 日 (三) 10:14 差异 历史 -3 m 区间 (同伦类型论) 消歧义 当前
- 2023 年 5 月 24 日 (三) 10:12 差异 历史 -439 m 模板:类型论 去掉一些不那么重要 (又已经写完, 因此不需要在写作计划里面出现) 的词条的索引 当前
- 2023 年 5 月 24 日 (三) 10:05 差异 历史 0 m 非直谓性 (类型论) typo
- 2023 年 5 月 24 日 (三) 10:03 差异 历史 +969 m 非直谓性 (类型论) 大幅改进
- 2023 年 5 月 24 日 (三) 09:02 差异 历史 +694 N 非直谓性 (类型论) 创建页面，并添加内容 “\textbf{非直谓性}一般来说是指某种定义是自指的, 在类型论中是|_(类型论)的性质. 大致来说, 若如下规则成立…”
- 2023 年 5 月 24 日 (三) 08:30 差异 历史 +517 N 区间类型 创建页面，并添加内容 “\textbf{区间类型}可以指: * \textbf{区间 (立方类型论)}, 立方类型论中用于定义相等类型的基础. 在双层类型…” 当前
- 2023 年 5 月 24 日 (三) 08:28 差异 历史 -108 m 谱 简化 latex 当前
- 2023 年 5 月 24 日 (三) 03:45 差异 历史 +31 m 用户:Ice1000/有向立方类型论 cite 当前
- 2023 年 5 月 24 日 (三) 00:12 差异 历史 +46 m 用户:Ice1000/综合代数几何 重新问了下
- 2023 年 5 月 24 日 (三) 00:10 差异 历史 +6 m 用户:Ice1000/综合代数几何 尴尬…手机太难用
- 2023 年 5 月 23 日 (二) 22:03 差异 历史 +22 m 用户:Ice1000/综合代数几何 wording
- 2023 年 5 月 23 日 (二) 20:46 差异 历史 +6 m 同伦类型论 Improve
- 2023 年 5 月 23 日 (二) 20:43 差异 历史 +192 m 等价 (类型论) 分段 当前
- 2023 年 5 月 23 日 (二) 20:41 差异 历史 +1,890 N 等价 (类型论) 创建页面，并添加内容 “\textbf{等价}在类型论中是函数类型实例的性质, 即给出一个 $\mathrm{isEquiv} : (A \to B) \to \operatorname{Prop}$, 命题宇宙保…”
- 2023 年 5 月 23 日 (二) 20:40 差异 历史 -1,707 m 泛等公理 提取内容 当前
- 2023 年 5 月 23 日 (二) 20:35 差异 历史 +74 m 用户:Ice1000/综合代数几何 Rua
- 2023 年 5 月 23 日 (二) 20:14 差异 历史 +137 m 用户:Ice1000/综合代数几何 改进
- 2023 年 5 月 23 日 (二) 20:03 差异 历史 +2,637 m 用户:Ice1000/综合代数几何 补全
- 2023 年 5 月 23 日 (二) 09:41 差异 历史 +1,140 N 用户:Ice1000/综合代数几何 创建页面，并添加内容 “无疑是本次旅行最大的惊喜. == 动机 == 使用类型论的方法研究代数几何. 想要的效果应该是类似同伦类型论中…”
- 2023 年 5 月 23 日 (二) 09:07 差异 历史 +78 m 用户:Ice1000 新增目录
- 2023 年 5 月 22 日 (一) 12:44 差异 历史 +3,456 N 用户:Ice1000/光滑无穷小分析 创建页面，并添加内容 “== 你懂吗 == \begin{definition} \textbf{方幂零元}或称\textbf{无穷小}是数 $ε$ 使得 $ε²=0$. 构造主义逻辑中, 该量不…” 当前
- 2023 年 5 月 22 日 (一) 11:57 差异 历史 0 m 用户:Ice1000/有向立方类型论
- 2023 年 5 月 22 日 (一) 11:55 差异 历史 +1,380 N 用户:Ice1000/有向立方类型论 创建页面，并添加内容 “在立方类型论中, 存在区间类型 $\mathbb I$, 这是一个双层类型论意义上的``准类型'' (exo-type). 在该区间类型上, 可以…”