Homotopy Type Theory / Univalent Foundations Zulip Chat

　　网址: https://hott.zulipchat.com/

　　特点: 这是当前HoTT领域最活跃、最核心的实时交流平台。几乎所有该领域的顶尖研究者、教授和博士生都在这里。讨论氛围非常专业且友好。

　　推荐频道:

　　#general: 用于发布你的核心问题。

　　#theory: 讨论类型论本身的基础问题。

　　#philosophy: 讨论数学哲学，非常适合你的“连续统幽灵”和“动态生成”问题。

　　#computer science 或 #PL: 讨论与编程语言、形式验证相关的应用。

　　Homotopy Type Theory Mailing List

　　网址: https://groups.google.com/g/homotopytypetheory

　　特点: 这是一个邮件列表，节奏比Zulip慢，但帖子通常更正式、更完整。适合发布长篇、深思熟虑的论述。

　　如何有效地提问和发起讨论

　　为了让你的想法获得最好的反馈，我建议你这样组织你的帖子：

　　标题示例:

　　Formalizing "Learning Types" and Dynamic Type Generation in HoTT?

　　Could HoTT describe a "becoming" process, not just a "being" state?

　　The "Continuous Ghost" in our Foundations: A question about discrete/finite alternatives to HoTT

　　内容结构建议:

　　清晰的背景陈述 (Brief Context):

　　"I've been thinking about how to formalize a lifelong learning AI system within a type-theoretic framework, and I've encountered a fundamental puzzle regarding the static nature of HoTT..."

　　核心问题 (The Core Problem):

　　清晰地描述“正在学习的类型”这一困境。使用你提出的 CanRecognizeCats 的例子。强调 HoTT 似乎只描述了状态的转换(¬P -> P)，而没有描述能力的 “生成事件” 本身。

　　与现有概念的连接 (Linking to Known Concepts):

　　这表明你做足了功课。可以这样写：“This seems related to the concept of Modal Type Theory (specifically temporal modalities), but I'm unsure if it fully captures the idea of a type universe that itself is expanding. It also reminds me of Open Type Theory and Reflection in programming languages.”

　　具体的问题 (Specific Questions for the Community):

　　提出明确的问题，引导讨论：

　　"Has there been any work on introducing a notion of 'real-time' or 'historical time' into HoTT, distinct from the 'proof-relevant' paths?"

　　"Is there a formalism that can describe the process of a new type being 'born' into the universe, perhaps through a meta-rule or an agent's action?"

　　"Could the Univalence Axiom be reinterpreted in a setting where the universe is not static but dynamically growing?"

　　分享你的初步构想 (Share Your Thought Experiment):

　　可以简要提及你“时间第一性”的数学思想实验，作为激发讨论的催化剂。例如："As a thought experiment, I've considered a foundation where the basic unit is not a static type but a rule executing in discrete time. Would such a 'process-first' approach be compatible with, or even help explain, the geometric intuitions of HoTT?"