dependent_type_theory

degree & universe

universe	type	term
$\mathcal U_{-1}$(Prop, Sort 0)	True	True.intro
$\mathcal U_{0}$(Type, Sort 1)	Bool	true
$\mathcal U_{1}$(Type 1, Sort 2)	Nat → Type	fun n => Fin n
$\mathcal U_{1}$(Type 2, Sort 3)	Type → Type 1	fun (_ : Type) => Type
…	…	…
universe, type, term为3种不同的度（degree）, 每个对象一定是其中的一种.
与集合论链式的$a \in b\in c\in d\dots$不同, 在类型中只有一条universe链和挂在上面的Type和Term, (这也暗示其实有时候即使类型论作为数学基础也要把集合那一套构造出来)
$$

\begin{CD}
\dots\
\mathcal U_n @<<< \text{Type in } \mathcal U_n @<<< \text{Term of type in } \mathcal U_{n+1} \ @VVV \
\mathcal U_{n+1} @<<< \text{Type in } \mathcal U_{n+1} @<<< \text{Term of type in } \mathcal U_{n+2}\
\dots
\end{CD}

$$
即使是type u参与的类型也只是一种类型, 而非宇宙~集合论中不能把(A, B)这个有序对和A $\times$ B这个笛卡尔积混淆, 即使AB中有元素

universe polymorphism

#check List
-- List.{u} (α : Type u) : Type u
universe u
def F (α : Type u) : Type u := Prod α α
#check F
-- 

实际上这里的u不是目标语言的项，应该把 Type u 看成一个整体
注意这是一般的依赖类型不包含的, 因为A: Type n必须要有个universe上限
能够写A: Type本质上也是这个原因, 实际上只是因为大部分时候只有有限个类型, 其宇宙必有上限

a ::
在要求自由变元显示闭包的情况下甚至可以不写universe u …a : Type u, 直接写a::, 甚至pi类型要用a直接写就行了, 有点类似于Haskell fmap :: (a -> b) -> f a -> f b(虽然Haskell不用显式定义闭包, 而是区分类型变量和值层（runtime）闭包)
也避免说Nat: Type和3: Nat这两种我觉得本质不同的东西

依赖类型

types can depend on parameters
如果类型签名写Type → α → List α → List α α的指代不清晰
建议写cons (α : Type) (a : α) (as : List α) : List α
/[[Public/fu_language]] cons α : Type : α → List α → List α
在 Haskell 中，cons 的类型是隐式多态的：cons :: α -> [α] -> [α]: 类型变量 α 由类型推断自动填充，无需显式传递 Type 参数。

dependent function type, or dependent arrow type, Pi-type:
α : Type and β : α → Type i.e. β: (a : α) → β a also writen as $\prod _{a :\alpha} ~\beta ~a$

dependent Cartesian product types (a : α) × β a also writen as $\sum _{a :\alpha} ~\beta ~a$
eg.godown := Sigma (λ n : Nat => Fin n) <2,1>:godown

依赖类型写法同一般的类型，如
F(a: A): phi a 等效于 F: (a:: A -> phi a)
a:: A, phi a

定义类型a:: A, phi a = b:: A, phi b// a，b只是个哑变元(否则不能反复声明类型)
a: A, …: phi a声明变量类型

eg. List a := True | a, List a
Nat := True | Succ Nat
Succ: (Nat -> Nat) 这里是自动转为 Succ Nat = n:: Nat, Succ n
_@_ f: (C <- B) g: (B <- A) = a:: A, b:: B, b = g a, c:: C, c = f b
(C <- B) @ (B <- A) = (C <- A)

a0::, Prod [[ = a0

每个类型可以看作一个关于自身良定义（可居性，存在一个对象）的命题
用Maybe单子修饰一个可能不存在的对象，如
a: Maybe A而不用提供A的良定义证明
因为Maybe A = True | A一定可居( 传统的True = None:: … )

//用“广义和类型”的方法(即n元组), 在lean中用的是类似函数的方法
//不能用函数(广义积类型), 因为只能证明对某个G有定义
monoid := G:: Type u, *:: (G -> G -> G), 1:: G,
	(assoc [*] [G]:= a b c:: G -> a * b * c = a * (b * c)),
	(one [*] [1] [G]:= a:: G -> a * 1 = a);
	
//
	
BinaryMonoid: monoid :=
	G := e | a,
	_ * _:={
	e * := _
	a * a := e},
	pf_mul_assoc:= ...,
	pf_mul_one:=...;

//证明部分还要学习

幂(函数/指数)类型

幂类型A->B
对象x=>f x
这里是是元语言(范畴论/λ演算)的概念, 其余都是由此导出, 在理论上用 Church 编码非常方便，因为我们只需要一个很小的核心语言就可以表达出许多复杂数据结构; 在工程语言中，更常用“原生的代数数据类型 + pattern matching”来获得更好的可读性和性能。
复合_@_ [A::Type, B::Type, C::Type]: (A<-B)->(B<-C)->(A<-C) := f => g=> x=> f g x
恒等函数 _ [A:: Type]:= x=>x

f(x: ℝ) : ℝ := x + 1; 这相当于一个语法糖, 不会真正声明变量x
//f := {x: ℝ -> x + 1} 括号防止命名空间污染
// f: := _ + 1: ℝ 这里相当于提升了1和+
// f: (ℝ -> ℝ) := _ + 1 这里 _ 的类型其实是 ℝ -> ℝ
_ f' := f;
// x f'
// _ f' x
// _ 表示输入变量且每一个不同 如 _ + _ = add
Do print (f' = f); //=>>True //只是表达方式不同

g x := {y := x ^ 2; 2 y};
g x := {2 y -| y := x ^ 2};
Do print type f;
//=>> ℝ -> ℝ
Do print g 1;
//=>> 2

积类型

• recursion：用归纳类型定义普通函数；
• induction：在依赖情形下，用归纳类型证明所有元素满足某种性质/构造依赖值
• 区别迭代iteration
  有两种方法，有点像所谓的内涵和外延，定义类型本身为构造出的项到currying后induction的像（church编码）；或定义一个构造子和induction（pattern match）。前者像是否等于codomain需要parametricity，我觉得这会使定义更自然

积类型A & B:= [R:: Type] -> (A → B → R) → R对于类型来说, R!=False, 总是存在的, 但这个类型签名并非全部, 必须要包含下面所谓的构造子(即一个到该类型的函数类型), 决定类型性质的是类型本身带有的结构（性质）,这种定义下本身就是消去规则
f: A->B->R a: A ,[R:: Type] b: B := f a b 存在性由笛卡尔闭范畴保证

a, b, c = a, (b, c)
括号只是用来区分优先级, 无实际作用
注意其他地方不要随便打逗号 eg. a b c : G -> a * b * c = a * (b * c)
所谓的构造子本身即到对应类型的函数，决定类型性质的是类型本身带有的结构（性质）,这种定义下本身就是消去规则

]] [[L: Type]] [R:: Type] l: L r: R := r 这(right)其实也有人叫true, 也算一种双关梗了
同理 …
]] (a, b) == b, [[ (a, b) == a, [[ 2 ]] (0, 1, 2, 3) == 2 这里用的自然数代表将函数作用几次的定义

之所以用符号, | ->是因为往往构造的是对应类型的对象, 并非同一类型的操作，即a,b和a不是同一类型
保留+ * ^用于同一类型

/ 自然变换
/ 等于即等价，但有不同路径
$A \times B = B \times A \implies left (A \times B) = \sigma left\sigma(B \times A)$

和(余积)类型

和类型 A | B:= [R:: Type] (A -> R) -> (B -> R) -> R
存在性同样需要额外的公理
(]] _ _ a: A): A | B 和类型中这里的]]输入函数类型
同理…
如果AB不同其实是可以自动匹配左右的
/ 语法糖(f , g) a

导出类型

/ True := [R: Type] & a:: R-> b:: R-> a = b单元集，存在性由R的良定义保证
List a: Type := True | a & List a
Nat := 0 ^ | succ ^ Nat
0 f := _
succ := n:: Nat => f=> x=> f n f x
[R: Type] a: R ^ :=b:: R & b = a
f: R->T ^ [T: Type] R:Type := t: T & r: R & t = f r

命题截断 (n = -1)

类型： ‖ A ‖ 或 ∥ A ∥ 或 Trunc (-1) A
含义： 将类型 A 变成一个命题。它表达的逻辑是 “A 是否可被证明”，或者说 “A 是否 inhabited”。
构造子：
|_| : A → ‖ A ‖：如果 A 有一个实例 a : A，那么 ‖ A ‖ 就为真（通过 | a | 证明）。
关键性质（消去规则）： 为了从 ‖ A ‖ 证明另一个命题 P，你只需要证明 A → P。因为 P 是命题，所以具体是 A 中的哪个 a 证明的并不重要。

rec : (A → P) → isProp P → ‖ A ‖ → P

这完美地对应了逻辑中的存在量词的消去规则：如果你知道 ∃ x, A(x)，并且你想证明一个命题 P，你只需要证明对于任意一个 x 满足 A(x)，都能推出 P。