首页/论文/2008.12433

arXiv 2008.124332020-08math.LOmath.CT

同伦类型论中的2-伴随等价

2-adjoint equivalences in homotopy type theory

Daniel Carranza, Jonathan Chang, Chris Kapulkin, Ryan Sandford

发表信息：: Logical Methods in Computer Science, Volume 17, Issue 1 (January 22, 2021) lmcs:6778
DOI：: 10.23638/LMCS-17(1:3)2021

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

AI总结：

本文在同伦类型论中定义（半）2-伴随等价并证明其性质，且已在Lean中形式化验证。

摘要：

我们在同伦类型论中引入了（半）2-伴随等价的概念，并证明了其预期性质。我们在Lean定理证明器中形式化了这些结果。

英文摘要：

We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

将同伦等价与带计算公理的依赖类型理论中的保守性联系起来

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms

本文借助同伦类型理论与带属性范畴，通过上下文间典范同伦等价证明外延类型理论对带命题计算公理的依赖类型理论具有保守性。

2025-09-25cs.LOmath.CTmath.LO

图的真同伦等价的复杂性

The Complexity of Proper Homotopy Equivalence of Graphs

该研究证明局部有限图的真同伦等价关系是博雷尔完全的，发现无限图中存在comeager等价类，并由此推出带裤子分解的非紧曲面同胚关系的类似结论。

2025-11-12math.GNmath.GTmath.LO

同伦类型论中环面与两圆乘积的等价性

The equivalence of the torus and the product of two circles in homotopy type theory

同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。

2015-10-13cs.LOmath.LO

内部和局部同伦理论

Internal and local homotopy theory

在Grothendieck topos中有一个关于单纯对象的完善的同伦理论，民间传说说弱等价在$L_{ω_1, ω}$的几何片段中是可公理化的。我们表明，它实际上是一个理论的预层型，即分类的预层拓扑。作为推论，我们得到了一个新的证明，证明了作为局部弱同伦等价的单纯预层的局部Kan纤维化正是具有期望的局部提升性质的态射.

2014-04-30math.ATmath.CTmath.LO

自伴算子的酉等价模紧的Weyl-von Neumann定理和Borel复杂性

Weyl-von Neumann Theorem and Borel Complexity of Unitary Equivalence Modulo Compacts of Self-Adjoint Operators

Weyl-von Neumann定理证明了Hilbert空间$H$上的两个有界自伴算子$A,B$是酉等价的模紧，即，对于某些酉$u\in \mathcal{U}(H)$和紧自伴算子$K$，当且仅当$A$和$B$具有相同的本质谱：$σ_{\rm{ess}}(A)=σ_{\rm{ess}}(B)$。在本文中，我们考虑在何种程度上可以（不）扩展到无界算子的描述集理论的Weyl-von Neumann的结果。我们表明，如果$H$是可分的无限维，有界自伴算子的等价关系是光滑的，而一般的自伴算子的等价关系包含一个密集的$G_δ$ -轨道，但不允许分类的可数结构。另一方面，显然相关的等价关系$A\sim B\Leftrightarrow \exists u\in \mathcal{U}(H)\ [u(A-i)^{-1}u^*-(B-i)^{-1}$是紧凑的]，是光滑的。各种Borel或co-analytic等价关系相关的自伴算子也被提出。

2014-02-27math.FAmath.LOmath.OA

关于与自伴算子有关的Borel等价关系

On Borel equivalence relations related to self-adjoint operators

在最近的工作中，作者研究了波兰空间${\rm{SA}}(H)$上定义的所有（不一定有界）自伴算子在可分无限维希尔伯特空间$H$上的各种Borel等价关系。本文研究了由$AE_{\rm{dom}}^{\rm{SA}(H)}B\Leftrightarrow {\rm{dom}}{A}={\rm{dom}}{B}$给出的域等价关系$E_{\rm{dom}}^{\rm{SA}(H)}$，并确定了它的精确Borel复杂度：$E_{\rm{dom}}^{\rm{SA}(H)}$是一个$F_σ$（而不是$K_σ$）等价关系，它与$\mathbb{R}^{\mathbb{N}}$上标准Borel群$\ell^{\infty}=\ell^{\infty}(\mathbb{N},\mathbb{R})$的轨道等价关系$E_{\ell^{\infty}}^{\mathbb{R}^{\mathbb{N}}}$是连续双可约的.根据Rosendal定理，这表明$E_{\rm{dom}}^{\rm{SA}(H)}$对于PDMATHAMR等价关系是普适的。此外，我们证明了一般的自伴算子有纯奇异连续谱等于$\mathbb{R}$。

2014-09-08math.FAmath.LOmath.SP