符号表

符号读作意义
$x \mapsto b(x)$$x$ maps to $b(x)$$\lambda x . b(x)$
$f \sim g$$f$ is homotopy to $g$$\Pi_{(x:A)}f(x) = g(x)$
$A ≃ B$$A$ is equivalence to $B$$\Sigma_{(f:A→B)}\text{is-equiv}(f)$
$p^{-1}$inverse of path $p$$(\Pi_{(x,y:A)} (x = y) → (y = x))(p)$
$A ↪ B$$A$ is embedding to $B$$Σ_{(f : A → B)} \text{is-emb}(f)$
$A ≅ B$$A$ is isomorphism to $B$isomorphisms of (semi)groups from $A$ to $B$
$A/R$$Σ_{(P:A→Prop)}\text{is-equivalence-class}(P)$

定义

Equals

Judgemental equal

基本上就是“按照定义相等”，“语义上相等”的意思。

比如 $2 \doteq 2$, $2 \doteq suc(suc(0))$.

一般来说，judgemental equal 都是根据某些假定(postulate) 做出来的，比如最常见的每个东西 judgemental equal 自己，每个东西 judgemental equal 它的定义，以及 $\Pi$ 上的计算规则（我只写了最终结论，请自行补全 deduction tree）：

$$ (\lambda y.b(y))(x) \doteq b(x) : B(x) $$

$$ \lambda x.f(x) \doteq f : \Pi_{(x:A)} B(x) $$

都是利用假定的一些规则形成 judgemental equal 的例子。

$\doteq$ 具有交换率和结合率。

In Agda, 所有能被 type checker 自动 “转换” 的东西之间都是 judgemental equal 的，比如你可以在一个要求放入函数 $f$ 的地方放入 $\lambda x . f(x)$，类型检查器不会 complain，因为它们 judgemental equal。

Propositional equal/identity type

由于 judgemental equal 有很多限制，比如依照下面的自然数定义，我们不能证明 $add(0, n) \doteq n$，因此需要引入 propositional equal。

根据 Curry-Howard correspondence，两个值相等这一个命题可以被转化为一个类型，这就是 propositional equal 类型，或者称为 identity type。

注意我们定义出来的 identity type 是依附于某个点上的，比如对于 $a : A$，我们可以定义 $a =_A x$ 是 $A$ 类型在 $a$ 点上的 identity type，它是一个依赖于 $x$ 的类型 （可以写作 $Id_a(x)\ type$）。

Identity type 具有交换率和结合率。

Observational equal

单纯地定义 identity type 只是使得“某两个东西相等”可以被表示，目前我们只有 $refl_x : x = x$ 这一种 “形成” identity type 的项的方式，这显然是不够的。

有时，我们可以在某个类型上定义出一个二元关系，然后将 $R(x, y)$ 映射到 $\top$ 或 $⊥$，然后利用这个关系来定义 构造 identity type。

比如对于自然数，我们定义二元关系 $\text{Eq-N}$：

$$ \text{Eq-N} : N → N → Set $$ $$ \begin{align} \text{Eq-N}&(&0 &,& 0 &)& & := ⊤ \\ \text{Eq-N}&(&0 &,& suc(n) &)& & := ⊥ \\ \text{Eq-N}&(&suc(n) &,& 0 &)& & := ⊥ \\ \text{Eq-N}&(&suc(m) &,& suc(n)&)& & := \text{Eq-N}(m, n) \end{align} $$

然后将这种关系和 identity type 关联起来：

$$ \text{Eq-N-refl}: (n : N) → \text{Eq-N}(n, n) $$ $$ \begin{align} \text{Eq-N-refl} &(&zero &)& & := tt \\ \text{Eq-N-refl} &(&suc(n)&)& & := \text{Eq-N-refl}(n) \end{align} $$ $$ \text{identity-to-Eq-N} : (x : N) → (y : N) → x ≡ y → \text{Eq-N}(x,y) $$ $$ \begin{align} \text{identity-to-Eq-N}(x,x,refl_x) & := \text{Eq-N-refl}(x) & \end{align} $$ $$ \text{Eq-N-to-identity} : (x : N) → (y : N) → \text{Eq-N}(x,y) → x ≡ y $$ $$ \begin{align} \text{Eq-N-to-identity} &(&0 &,& 0&,& eqnxy) & := refl \\ \text{Eq-N-to-identity} &(&suc(x)&,& suc(y)&,& eqnxy) & := cong(suc,\text{Eq-N-to-identity}(x,y,eqnxy)) \end{align} $$

Induction (归纳)

就是定义了一个基本 case 满足某些性质，然后定义了一个如何根据某个 case 推导出下一个 case 的规则，然后就可以推导出所有的 case 都满足这个性质。

以下是一些书中提到的例子：

自然数

  • base case: $p_0 : P(0)$
  • inductive case: $p_s : \Pi_{(n : \mathbb{N})} P(n) \rightarrow P(suc(n))$
  • induction: $ind_{\mathbb{N}}(p_0, p_s) : \Pi_{(n : \mathbb{N})} P(n)$

其中 $P$ 代表参数具有的性质。

通过 $ind_{\mathbb{N}}$，我们可以定义出加法：

  • base case: $p_0 := m$
  • inductive case: $p_s := \lambda n . suc(n)$
  • induction: $add(m, \underline{}) := ind_{\mathbb{N}}(p_0, p_s)$

因此，根据 add 的定义，我们可以得到：

  • $add(m, 0) \doteq m$ 是一个 judgemental equal。
  • $add(m, suc(n)) \doteq suc(add(m, n))$ 是一个 judgemental equal。

但是，我们不能得到 $add(0, n) \doteq n$，这是 judgemental equal 的一个限制。

unit 类型（⊤）

只有 1 个 term 的类型。

$$ ind_\top: P_{tt} → \Pi_{(x : \top)} P(x) $$

$$ ind_\top(p, tt) := p $$

变种：singleton induction

由于 contractable type 在 homotopy 意义上是一个 singleton，我们可以用和 unit type induction 类似的方法定义 singleton induction。

$$ ind_{\text{singleton_a}} : P_{a} → \Pi_{(x : A)} P(x) $$

如果在一个非空的类型上能定义出这样一个 singleton induction 函数，那么这个类型就是 contractable 的，反之亦然。

空类型（⊥）

没有 term 的类型。

$$ \bot\text{-elim} := ind_\bot : \bot → A $$

和类型/余积类型

$$ ind_+ : (\Pi_{(x:A)} P(inj_1(x))) → (\Pi_{(y:B)} P(inj_2(y))) → (\Pi_{(z:A⊎B)} P(z)) $$ where $$ ind_+(f, g , inj_1(x)) := f(x) $$ $$ ind_+(f, g , inj_2(y)) := g(x) $$

pair 类型 / Σ 类型

$$ ind_\Sigma : (\Pi_{(x : A)} \Pi_{(y : B(x))} P(x, y)) → \Pi_{(z : Σ_{(x : A)} B(x))} P(z) $$ $$ ind_\Sigma(g, (x, y)) := g(x, y) $$

我们当然可以定义出 B 类型不依赖于 A 类型的特殊情况，即积类型：

$$ ind_\times : (\Pi_{(x : A)} \Pi_{(y : B)} P(x , y)) → \Pi_{(z : A \times B)} P(z) $$ $$ ind_\times(g, (x, y)) := g(x, y) $$

Propositional equal 类型 / identity 类型 / Path 类型

$$ ind_{=_a} : P(a, refl_a) \rightarrow (\Pi_{(x : A)} \Pi_{(p:a=x)} P(x, p)) $$ $$ ind_{=_a}(u, a, refl_a) := u, \text{where}\ u : P(a, refl_a) $$

基本上就是说，如果某个特性在 $(a, refl_a)$ 上成立，那么它在任意 $(x, p)$（其中 $p$ 是 $a = x$ 的证据，也称 $a$ 到 $x$ 的一条 path）上都成立。

这也被称为 path induction。

再次提醒注意，这里的 $a$ 是 “钉死” 的。

Homotopy

$$ ind_{htpy} : (\Pi_{(g: \Pi_{(x:A)}B(x))}\Pi_{(H: f \sim g)}P(g,H)) → P(f, \text{refl-htpy}_f) $$

$$ ind_{htpy}(s, f, \text{refl-htpy}_f) := s(f, \text{refl-htpy}_f) $$

fiber

$$ fib_f(b) := \Sigma_{(a : A)} f(a) = b $$

对应了 b 在 f 上的原像。

pointed type

Basically a type with a point.

The type of a pointed type is: $$ \mathcal{U}_* := Σ_{(A : \mathcal{U})} A $$

An example of a pointed type is $(ℕ , 0)$. Pointed maps are maps between pointed types that preserve the point.

$$ (A →_* B) := Σ_{(f : A → B)} f(a) = b $$

loop space

$$ \begin{align} \Omega & : \mathcal{U}_* → \mathcal{U}_{*} \\ \Omega(A, a) & := (a = a, \text{refl}) \end{align} $$

We can apply $\Omega$ multiple times to get iterated loop spaces:

$$ \begin{align} \Omega^0(A, a) & := (A, a) \\ \Omega^1(A, a) & := \Omega(A, a) \\ \Omega^2(A, a) & := \Omega(\Omega(A, a)) \\ ⋯ \\ \Omega^{n+1}(A) & := \Omega(\Omega^n(A, a)) \end{align} $$

类型/函数的属性

is-empty

$$ \text{is-empty}(A) := A → \bot $$

sec/retr

假设 $f : A → B$，sec 表示函数存在右逆。

$$ \text{sec}(f) := \Pi_{(g:B→A)} f ∘ g \sim id $$

retr 表示函数存在左逆。

$$ \text{retr}(f) := \Pi_{(h:B→A)} h ∘ f \sim id $$

retr 之所以称为 retr，是因为 $h$ 可能只是将 B 的一个子集(即 $f$ 的像)映射到了 A 。此时我们就说 A 是 B 的一个收缩（retraction）。

is-equiv

$$ \text{is-equiv}(f) := sec(f) \times retr(f) $$

$$ \text{is-equiv}(f) := \Sigma_{(g : B → A)} (f \circ g = id_B) \times (g \circ f = id_A) $$

重要的等价关系

  • For an equivalence relation $R$: $$ ([x]_R = [y]_R) ≃ R(x, y) $$
  • symmetry of equality $$ (x = y) ≃ (y = x) $$
  • concat on path $p: x = y$ $$ 𝑝⋅- : (𝑦 = 𝑧) ≃ (𝑥 = 𝑧) $$ $$ -⋅q : (𝑥 = 𝑦) ≃ (𝑥 = 𝑧) $$
  • transport on path $p: x = y$ $$ tr_𝐵(𝑝) : 𝐵(𝑥) ≃ 𝐵(𝑦) $$
  • any section and any retraction of an equivalence is again an equivalence.
  • equivalent types have equivalent identity types ($e : A ≃ B$, then $ap_e$ is an equivalence function)
  • "axiom" of choice $$ \begin{align} choice &: & \Pi_{(x:A)}\Sigma_{(𝑦:𝐵(𝑥))}𝐶(𝑥, 𝑦) ≃ \Sigma_{(𝑓:\Pi_{(𝑥:𝐴)} 𝐵(𝑥))}\Pi_{(𝑥:𝐴)}𝐶(𝑥, 𝑓(𝑥)) \\ choice(h) &:= & (𝜆𝑥. pr_1(h(𝑥)), 𝜆𝑥. pr_2 (h(𝑥))) \end{align} $$
  • $sec(pr_1) ≃ \Pi_{(𝑥:𝐴)} 𝐵(𝑥)$

is-contr

$$ \text{is-contr}(A) := \Sigma_{(c : A)} \Pi_{(x : A)} c = x $$

$$ \text{is-contr}(f) := \Pi_{(b : B)} \text{is-contr}(fib_f(b)) $$

We call $f$ a contractible map.

$$ \text{is-contr}(f) ↔ \text{is-equiv}(f) $$

Important contractible types

  • $⊤$
  • $⊥$
  • $Σ_{(x:A)} a = x$
  • Product of contractible types is contractible
  • Observational equal on $ℕ$, $Bool$ and coproduct type, ie. $\text{Eq-N}(n,m)$. with one of n and m fixed by $\Sigma$, ie. $\Sigma_{(n:N)} \text{Eq-N}(m,n)$
  • A type $A$ is contractible if and only if the identity map on $A$ is constant.
  • A map is an equivalence if and only if its fibers are contractible

is-coh-invertible

对于一个函数 $f : A \rightarrow B$, 如果他是一个 equivalence, 其逆为 $g$, $g$ 为右逆的证据为 homotopy $G$, $g$ 为左逆的证据为 homotopy $H$，同时存在 Homotopy $K : G \cdot f \sim f \cdot H$，我们称 $f$ 为 coherently invertible map。

$$ \text{is-coh-invertible}(f) := \Sigma_{(g : B → A)} \Sigma_{(G : f \circ g \sim id_B)} \Sigma_{(H : g \circ f \sim id_A)} \Sigma_{(K : G \cdot f \sim f \cdot H)} (g, G, H, K) $$

Any coherently invertible map is a contractible map.

is-emb

$$ \text{is-emb}(f) := (x, y : A) → \text{is-equiv}(cong\ f\ {x}\ {y}) $$

is-prop

$$ \text{is-prop}(A) := \Pi_{(x,y : A)} \text{is-contr}(x = y) $$

Identity types on A are contractable.

or

$$ \text{is-prop}(A) := \Pi_{(x,y : A)} x = y $$

Any two terms on A are equal.

$$ \text{is-prop}(A) := A \rightarrow \text{is-contr}(A) $$

A is not empty and contractable (can be contracted to the given point).

Important props

  • Everything is contractible type is a prop.
  • If $A$ is a prop, $A ≃ B$, then $B$ is a prop. And vice versa, all props are equivalent to each other.s
  • Observational equal on $ℕ$ and Bool, ie. $\text{Eq-N}(n, m)$. Since it is equivalent to identity type on these types, identity type on these types is also a prop.
  • A product of props is a prop.
  • Given a prop A and $\text{is-subtype}(B)$ of A, then $\text{is-prop}(Σ_{(x:A)} B(x))$
  • $\text{is-emb}$, $\text{is-surj}$ and $\text{is-equiv}$.
  • $\text{is-contr}(A)$, $\text{is-prop}(A)$ itself, $\text{is-set}(A)$, ..., $\text{is-trunk}_k(A)$ is a prop.
  • Given a prop B, $A → B$ is a prop, a special case is, the negation of a type ($\neg A$) is a prop.
  • $\text{is-unital}(G)$, $\text{is-group}(G)$, for any semigroup $G$.
  • A map $f : A → B$ is an embedding if and only if its fibers are propositions.
  • A type 𝐴 is a proposition if and only if the identity map on 𝐴 is weakly constant ($\Pi_{(x,y:A)} f (x) = f (y)$).

is-subtype

$$ \text{is-subtype}(B) := (x : A) → \text{is-prop} (B(x)) $$

We say $B$ is a subtype of $A$.

is-set

$$ \text{is-set}(A) := \Pi_{(x,y : A)} \text{is-prop}(x = y) $$

is-trunc-k

$$ \begin{align} \text{is-trunc}_{-2}(A) & := \text{is-contr}(A) \\ \text{is-trunc}_{k+1}(A) & := \Pi_{(x,y:A)}\text{is-trunc}_k(x = y) \end{align} $$

a map $f : A → B$ is k-truncated if its fibers are k-truncated.

  • Product ($\Pi$) of k-truncated types is k-truncated.
  • retract of k-truncated type is k-truncated
  • $f: A→B$, B is 𝑘-type, then "A is k-type" ↔ "f is k-type"
  • If $𝑓 : 𝐴 → 𝐵$ is an embedding, and 𝐵 is a (𝑘 + 1)-type, then so is 𝐴.
  • 𝑓 is (𝑘 + 1)-truncated, then $ap_f$ is k-truncated, and vice versa.
  • 𝐵(𝑥) is 𝑘-truncated for each $𝑥 : 𝐴$ ↔ $Σ(𝑥:𝐴) 𝐵(𝑥)$ is 𝑘-truncated

is-small

$$ \text{is-small}_{\mathcal{U}}(A) := Σ_{(X:\mathcal{U})} A ≃ X $$

for a map $f : A → B$, $f$ is small if all its fibers are small.

is-locally-small

$$ \text{is-locally-small}_{\mathcal{U}}(A) := \Pi_{(x, y : A)} \text{is-small}(x = y) $$

for a map $f : A → B$, $f$ is locally small if all its fibers are locally small.

All small types are locally small in the same universe.

Any proposition is locally small in any universe.

Any univalent universe U is locally U-small.

is-equivalence-class

For $R$ to be an equivalence relation, a subtype $P : A → Prop$

$$ \text{is-equivalence-class}(P) := ∃(x:A)∀(y:A) P(y) ↔ R(x, y) $$

is-effective

For $R$ to be an equivalence relation,

$$ \text{is-effective}(f) := (x, y : A) → (f(x) ≡ f(y) ≃ R(x, y)) $$