Plans

Author: Trebor-Huang

identity.typ

@@ -77,7 +77,7 @@ $)
   给定两个类型 $A$ 与 $B$，其间的*等价*是函数 $f : A -> B$，配有左逆 $g : B -> A$ 使得 $g compose f = id$，与右逆 $h : B -> A$ 使得 $f compose h = id$。记全体等价构成的类型为 $A tilde.eq B$。
 ] <def:equivalence>
 
-这里，我们不要求左逆与右逆相同，因为如果做此要求，相当于额外提供一条道路 $p : "Id"(B -> A, g, h)$，是额外的资料。但是如此定义等价之后，可以另外证明 $forall b bind g(b) = h(b)$。这样定义的好处是，给定某个函数 $f$，等价中其余的数据构成命题，即至多有一种方法将其补全为等价。 HoTT 书~@hott-book 中也有其它的等价定义。
+这里，我们不要求左逆与右逆相同，因为如果做此要求，相当于额外提供一条道路 $p : "Id"(B -> A, g, h)$，是额外的资料。但是如此定义等价之后，可以另外证明 $forall b bind g(b) = h(b)$。这样定义的好处是，给定某个函数 $f$，至多有一种方法将其补全为等价。HoTT 书~@hott-book 中也有其它的等价定义。
 
 给定某个宇宙 $cal(U)$ 中两个类型的名字 $A, B : cal(U)$，如果有 $p : "Id"(cal(U))$，那么可以给出函数 $A -> B$ (将类型的名称 $A : cal(U)$ 与类型本身 $"El"(A) istype$ 混同)：利用 J 原理，只需给出一个函数 $A -> A$ 即可，而恒等函数 $id$ 满足条件。这个函数同时还总是等价，因此这就给出了映射 $(A = B) -> (A tilde.eq B)$。关于宇宙 $cal(U)$ 的*泛等公理*说的是这个映射本身是等价。
 

syntax.typ

@@ -1,13 +1,24 @@
 #import "common.typ": *
 = 语法性质的证明 <ch:syntax>
 
-- warm up: true is not equal to false
+- warm up: true is not equal to false using Set models
 
 == 典范性
-- technique of gluing (dependent elimination)
+- direct construction of the model
+  - "tracking elements", pretending simple types
+  - contexts are $(X, Gamma, sigma : X -> hom(1, Gamma))$, types are $(Y_(x in X), A, Y_x -> A sigma_x)$, elements are a tracking element together with a corresponding real element
+
+- dependent elimination, displayed models and gluing
 
 == 正规性
-  - judgmental injectivity of type constructors
+
+- direct construction of the mode
+  - Tracking elements are equipped with renaming action
+  - Presheaf of normal and neutral forms
+- algorithmic content and decidability of judgmental equality (of well-typed terms)
+  - This gives decidability of typechecking, but is tricky
+- judgmental injectivity of type constructors
 
 == 参数性
+- Discuss models of system F?
 - distinguish syntactic and set-semantic parametricity