Typed structures

维护 Spore Notation 语言设计稿。理论结构与实际数据结构一起引入，并提供对应的操作和 law 证据；没有与本稿对应的类型检查器或证明内核。

工作方式

从 examples.md 选择相关章节：01 定义与宇宙，02 子类型，03 精化，04 范畴与元组，05 计算结构与 Option，06 序列，07 映射，08 索引类型。它们按依赖顺序共享背景，不为小改动加载全部证明。
写程序时以以下规则为准，对照 grammar.ohm 检查表面形式。用户提出新设计时区分既有规则与提案，不为兼容旧例子恢复废弃语法。
新写或改写的程序先写入文件并做句法检查；另行审阅宇宙、态射起终点、泛型作用域、Self、继承字段与 law。文法不决定这些语义。
报告实际完成的检查。用户明确要求其他语言实现时遵从目标；该实现的运行结果不构成本稿的机器证明。

采用非累积宇宙与宇宙多态：Universe<u>: Universe<next(u)>;、Prop = Universe<0>;、Type = Universe<1>;。首行是背景规则模式，不是 Universe 属于自身的定义。
层级支持 next/max，数字是 next 迭代的简写；层级不是运行时 Nat。省略层级或写 _ 产生待推断变量；声明中独立且未固定的层级可以推广，调用时实例化。不能把一次推断当成任意层级通用，不自动提升或降低宇宙。
依赖函数的数据层级按输入与结果的 max 计算；结果是命题时，对任意宇宙量化仍属于 Prop。区分 A -> P 与返回命题类型的 A -> Prop。不据此引入证明无关、擦除或任意从 Prop 向数据消去。
<u> 用于层级，[A: Type, n: Nat] 用于泛型或索引，(x, y) 用于普通实参。[A] 默认绑定 A: Type；结构值参数也放在 []，例如 F: Functor[C,D]。
普通多参数函数不自动柯里化。(A, B) -> C 与 A -> B -> C 用显式 curry / uncurry 对应。(pair: (A,B)) -> C 接收一个元组；调用写 f((a,b))，不自动拆包或引入 <a,b> 调用形式。