Homotopy Type Theory: A synthetic approach to higher equalities
Michael Shulman
这是对同伦类型理论和哲学家的单价基础的介绍，作为《工作哲学家的范畴》一书的一章（伊莱恩·兰德里编辑）。
This is an introduction to Homotopy Type Theory and Univalent Foundations for philosophers, written as a chapter for the book "Categories for the Working Philosopher" (ed. Elaine Landry)
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Coherence of strict equalities in dependent type theories
利用附加的严格等式研究了相关类型论扩张的凝聚性和保守性。通过考虑类型论模型的同馀项和同馀项的概念，我们重建了Hofmann关于外延类型论相对于内涵类型论的保守性的证明.我们推广这些方法的类型论没有统一的身份证明原则，如变种同伦类型论，通过引入一个概念，更高的同余模型的类型论。我们对更高全等的定义受到Brunerie对弱$\infty$ -群胚的类型论定义的启发。对于一个大类的类型论，我们减少了问题的保守性方程扩展到更易处理的无环性条件。
Synthetic Homology in Homotopy Type Theory
本文在同伦类型论中定义了同调，并在此过程中定义了稳定同伦群。合成同伦理论的研究依赖于以前的研究，特别是上同调的定义。这一工作为计算机检验同调结构奠定了基础。
Homotopy type theory: the logic of space
这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍，作为《数学和物理的新空间》（Gabriel Catren和Mathieu Anel编）一书的一章。
Synthetic Homotopy Theory
本论文基于同伦类型论（HoTT）系统阐述合成同伦理论，通过合成构造 Hopf 纤维化、证明 Blakers--Massey 定理、推导 Freudenthal 悬挂定理并计算 $n$-球面的部分同伦群，为代数拓扑研究提供了新的形式化方法。
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
高维重写系统是分析将项形式化约化为范式的结构以及比较导致这些范式的不同约化路径的工具。这种更高的结构可以通过找到重写系统的同伦基来捕获。我们表明，汇合和wellfoundedness的基本概念是足够的递归地建立这样一个同伦基础，与克雷格C。斯奎尔然后，我们继续翻译这个建设的同伦类型论的设置，其中管理路径之间的等式是很重要的，以构建功能是一致的，就更高的维度。最后，我们应用这个结果来近似同伦类型论中的一系列公开问题，例如集合上自由群的同伦群的特征和1-类型的推出。本文扩展了我们以前的会议贡献“通过良好的一致性”（arXiv：2001.07655），通过布局的语言更高的维度重写的建设。
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
本论文的目的是在同伦型理论的背景下提出综合同伦理论。我们将提出各种结果在这个框架中，最值得注意的是建设的Atiyah-Hirzebruch和塞尔谱序列的上同调，已完全正式的精益证明助手。
Classifying Types
在类型论的语言中，同伦理论现象的研究有时被称为“合成同伦理论”。同伦类型论中的同伦理论只是同伦类型论的众多方面之一，同伦类型论还包括集合论语义的研究（同伦类型论模型和集合或范畴的元理论中的单值性），类型论语义学（同伦类型理论的内模）和计算语义学，以及研究同伦类型理论内部语言中的各种问题，这些问题不一定是由同伦理论激发的，或与基于同伦类型理论的形式化数学库的发展相关的问题。本论文是关于综合同伦理论的发展。
Impredicative Encodings of (Higher) Inductive Types
本文针对依赖类型论中非直谓编码缺乏 η-等式和依赖消去的问题，提出基于同伦类型论的精化构造方法，并将其扩展至高阶归纳类型如 1-截断和单位圆 S1。
Homotopy type theory as a language for diagrams of $\infty$-logoses
论文展示通过扩展同伦类型论加入某些lex可及模态量，可将∞-逻辑格的图示重构，从而用普通同伦类型论处理单个或多个∞-逻辑格。
Homotopy Type Theory in Lean
我们在精益证明助手中讨论同伦类型论库。该图书馆特别面向合成同伦理论。特别令人感兴趣的是使用了一些高级归纳类型的原始概念，即截断和截断，以及立方方法的使用。
Classical field theory via Cohesive homotopy types
经典场论如何在凝聚同伦型理论中综合出现的简要综述。扩展的会议摘要提交给2013年秋季在巴塞罗那举行的类型理论，同伦理论和单价基础会议的会议记录
A Foundation for Synthetic Stone Duality
本文以扩展 4 条公理的同伦类型论为轻凝聚集高阶 topos 的内部语言，建立合成拓扑与上同调工具，并内部证明 Brouwer 不动点定理。
Generalized Chevalley criteria in simplicial homotopy type theory
本研究在Riehl–Shulman单纯同伦类型论框架下，将（余）笛卡尔箭头、纤维化与函子的经典条件推广为以任意形状包含替代端点包含的广义形式，为合成内蕴$(\u221e,1)$-范畴论研究提供了新的处理方式。
Synthetic Spectra via a Monadic and Comonadic Modality
我们扩展同伦类型理论与一个新的模态，同时是单子和comonad。因为这种模态在每一个类型上都诱导了一个非平凡的内映射，所以它需要一个比同伦类型论以前的模态扩展更复杂的判断结构。我们使用这个理论来开发一种光谱的合成方法，其中光谱由某些类型表示，并且通过类型结构来构建它们：谱的映射由普通函数表示，闭路空间由单位类型表示，等等。我们用一对公理扩充了类型论，其中一个公理意味着谱是稳定的，另一种是把合成谱与类型论中谱的普通定义联系起来，称为$Ω$ -谱。最后，我们表明，类型理论是健全的和完整的抽象范畴语义，在范畴与家庭的弱自同态函子的上下文中是一个双反射，即有一个counit一个单位，是一个部分收缩对。
The equivalence of the torus and the product of two circles in homotopy type theory
同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。
The HoTT Library: A formalization of homotopy type theory in Coq
我们报告的HoTT库的发展，同伦类型论的形式化Coq证明助手。它形式化了大多数基本的同伦类型论，包括单值性、高级归纳类型、大量的综合同伦理论，以及范畴论和模态。该图书馆已被用作几个独立开发的基础。我们讨论的决定，导致图书馆的设计，我们评论同伦类型论的相互作用与最近推出的功能Coq，如宇宙多态性和私人归纳类型。
A Synthetic Perspective on $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects
推理弱的高级范畴结构构成了一项具有挑战性的任务，即使是专家。一个主要的原因是集合论的语言在较弱的等价概念下不是不变的，比如同伦等价。从这个角度来看，要求一个更自然地支持这些概念的不同的基础环境是很自然的。我们的工作采取了建议，在原来的文章arXiv：1705.07442由Riehl-Shulman进一步发展合成$(\infty,1)$ -范畴论在单纯同伦型理论，特别是包括研究的cocarrhythmic纤维化。再加上一系列的分析结果，特别是由于里尔-维里蒂和Rasekh，因此，我们的类型理论帐户构成了一个合成理论的纤维化的内部$(\infty,1)$ -类别，w.r.t.通过Shulman关于单叶宇宙严格化的主要结果arXiv：1904.07004，我们得到了任意的Grothendieck-Rezk-Lurie- $(\infty,1)$ -topos。
Differential Geometry of Synthetic Schemes
该研究在综合代数几何框架下，利用同伦类型论给出概形间平展、光滑、非分歧映射的新综合定义，证明其微分刻画及光滑概形切空间性质，验证三类概形的局部代数描述的具体性。
Synthetic perspectives on spaces and categories
研究利用同伦类型理论和单纯类型理论，揭示在原生等价不变环境中关于空间和范畴的基本证明技术，包括路径或箭头归纳原理及相关构造。
Constructive higher sheaf models with applications to synthetic mathematics
本文提出了一种构造性高sheaf模型，用于合成数学中的类型理论扩展，包括univalence和高诱导类型，并构建了这些形式系统的构造性模型。
Commuting Cohesions
舒尔曼的空间类型理论将Lawvere的公理化内聚的模态内化为同伦类型理论，使得许多从Schreiber的模态方法到微分上同调的构造能够综合地进行。在空间类型理论中，每个类型在其点之间都具有空间内聚性，并且每个函数都是连续的。但在数学实践中，对象可以同时以不止一种方式是空间的;例如，单纯空间既有拓扑结构又有单纯结构。本文提出了一种具有“焦点交换”的类型理论，它允许类型携带多种空间结构。该理论是空间类型理论的一个相对轻松的扩展，并使我们能够综合考虑单纯的，微分的，等变的，和其他的凝聚力进行相同的类型。我们证明了理论表明，同伦类型的任何差分堆栈可以计算从一个离散的单纯集来自任何良好的覆盖的Čech神经。我们还给出了其他的例子交换凝聚力，如微分等变类型和超几何类型，奠定了基础的合成帐户Schreiber和Sati的适当orbifold上同调。
A type theory for synthetic $\infty$-categories
本文在同伦类型论中构建 $(\infty,1)$-范畴的综合基础，通过有向区间、Segal/Rezk 类型、协变纤维化及扩展类型刻画高阶范畴结构与伴随。
The Integers as a Higher Inductive Type
考虑了同伦类型论（HoTT）中整数的定义问题.我们可以将整数的类型定义为带符号的自然数（即，使用余积），但是它的归纳原理非常不方便使用，因为它导致了案例的爆炸。另一种方法是使用集合截断，但这里我们需要使用集合截断来避免非平凡的更高等式。这导致了一个递归原则，它只允许我们将函数定义为集合（满足UIP的类型）。在本文中，我们考虑使用小论域或双可逆映射的更高归纳类型。这些类型表示没有显式集截断的整数，等价于通常的余积表示。这是一个有趣的例子，因为它展示了如何在HoTT中处理一些一致性问题。我们讨论了这项工作引发的一些悬而未决的问题。证明已正式验证使用立方阿格达。
A Foundation for Synthetic Algebraic Geometry
本文基于Kock和Blechschmidt的工作，在Zariski topos内部建立代数几何基础，使用同伦类型论结合三个公理作为其内部语言，提出“Zariski局部选择”公理并通过立方模型证明其合理性，贡献了高阶类型在上同调推理中的应用。
Oracle modalities
本文以高阶模态重新表述 Turing 可归约性，在 cubical type theory 中借助 Markov induction 与 computable choice 公理给出综合证明，并初步建立 Turing 度与同伦论的联系。
Strict stability of extension types
本文通过Voevodsky分裂方法证明扩展类型在Riehl-Shulman同伦类型论中严格稳定，从而为内∞-范畴提供语义基础。
Semantics of higher inductive types
高阶归纳类型（英语：Higher inductive types）是一类类型形成规则，用来提供基本（和不那么基本）的同伦理论构造。他们已被证明是非常富有成效的“综合”发展同伦理论内的类型论，以及在形式化的普通集合层次数学的类型论。在这篇文章中，我们在相当广泛的设置中构建了各种各样的更高归纳类型的模型。我们引入细胞单子的概念与参数：一个语义定义的计划，指定同伦行为良好的结构概念。然后，我们表明，任何合适的模型类别有 * 弱稳定型初始代数 * 的任何细胞单子的参数。当与局部宇宙构造结合以获得严格稳定性时，它专门给出特定的更高归纳类型的模型，包括球体、环面、推出类型、截断、詹姆斯构造和一般局部化。我们的结果适用于任何足够好的Quillen模型范畴，包括任何右真的，单纯局部carrier-closed，单纯Cisinski模型范畴（如单纯集）和任何局部可表示的局部carrier-closed范畴（如集），其平凡模型结构。特别地，任何局部可表示的局部Carnival闭$(\infty,1)$ -范畴都由我们的结果所适用的模型范畴表示。
Classification of Covering Spaces and Canonical Change of Basepoint
本文基于同伦类型论证明了覆叠空间分类定理的综合版本，探讨了同伦群间基点典范变换同构的存在性，并使用Coq对证明进行了机械化。
Projective Space in Synthetic Algebraic Geometry
本文在合成代数几何框架下研究射影空间$\mathbb{P}^n$，证明其自同构群为$\mathrm{PGL}_{n+1}(R)$，皮卡德群为$\mathbb{Z}$，并给出线丛类型的精细描述。
Internal sums for synthetic fibered $(\infty,1)$-categories
本研究在单纯同伦类型论的合成设定下，将Moens定理等纤维化范畴理论结果推广到内蕴$(\u221e,1)$范畴的双纤维化情形，给出相关结构性刻画。
Modal Fracture of Higher Groups
本文研究了凝聚同伦类型论中高阶群的模态性质，提出模态破裂六边形将其分解为离散、无穷小和可缩成分，从而合成构造Schreiber微分上同调六边形，并推广至带连接的圆k-gerbe分类器。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。