Syntax table
| Syntax | Read as | Meaning |
|---|---|---|
| $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$ | isomorphisms of (semi)groups from $A$ to $B$ | |
| $A/B$ | $Σ_{(P:A→Prop)}is-equivalence-class(P)$ |
Definitions
Equals
Judgemental equal
Basically idea is "equal according to the definition" or "equal in terms of semantics."
eg. $2 \doteq 2$, $2 \doteq suc(suc(0))$.
In general, the only thing "judgmental equal" is based on is some certain assumptions (postulates). The most common ones include "everything being judgmentally equal to itself", "everything being judgmentally equal to its definition", and the calculation rules on $\Pi$ (I will write the final conclusion only, please complete the deduction tree on your own):
$$ (\lambda y.b(y))(x) \doteq b(x) : B(x) $$
$$ \lambda x.f(x) \doteq f : \Pi_{(x:A)} B(x) $$
are examples of forming "judgmental equal" using certain assumed rules.
The symbol $\doteq$ possesses trans and sym properties.
In Agda, anything that can be automatically "converted" by the type checker is judgmentally equal. For instance, you can replace a function $f$ with $\lambda x . f(x)$ in a context that expects the former, and the type checker won't complain because they are judgmentally equal.
Propositional equal/identity type
Due to the many restrictions of judgmental equality, such as in the definition of natural numbers below, where we cannot prove $add(0, n) \doteq n$, it becomes necessary to introduce propositional equality.
According to the Curry-Howard correspondence, the proposition that two values are equal can be translated into a type, known as the propositional equal type or identity type.
It's important to note that the identity type we define is associated with a specific point. For instance, given $a : A$, we can define $a =_A x$ as the identity type of type $A$ at the point $a$, which is a type dependent on $x$ (can be written as $Id_a(x)\ type$).
The identity type possesses trans and sym properties.
Observational equal
Simply defining the identity type allows us to express the notion of "two things being equal." Currently, we only have one way to "construct" an item of the identity type, which is $refl_x : x = x$, but clearly, this is not sufficient.
Sometimes, we can define a binary relation on a type and then map $R(x, y)$ to either $\top$ or $⊥$, using this relation to construct the identity type.
For example, for natural numbers, we can define a binary relation $\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} $$
Then associate this relation with the 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
It defines a base case satisfying certain properties and then specifies rules for deducing the next case based on a given case. This allows the deduction that all cases satisfy the specified property.
Here are some examples mentioned in the book:
Natural numbers
- 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)$
Where $P$ represents the property that the parameter possesses.
Through $ind_{\mathbb{N}}$, we can define addition:
- base case: $p_0 := m$
- inductive case: $p_s := \lambda n . suc(n)$
- induction: $add(m, \underline{}) := ind_{\mathbb{N}}(p_0, p_s)$
Therefore, according to the definition of add, we can obtain:
- $add(m, 0) \doteq m$ is a judgmental equal.
- $add(m, suc(n)) \doteq suc(add(m, n))$ is a judgmental equal.
However, we cannot deduce $add(0, n) \doteq n$, which is a limitation of judgmental equality.
unit type (⊤)
A type with only one term.
$$ ind_\top: P_{tt} → \Pi_{(x : \top)} P(x) $$
$$ ind_\top(p, tt) := p $$
empty type (⊥)
A type with no terms.
$$ \bot\text{-elim} := ind_\bot : \bot → A $$
Sum/Coproduct type
$$ 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 type / Σ type
$$ 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) $$
Of course, we can define a special case where type B does not depend on type A, namely, product types:
$$ 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 type / identity type / Path type
$$ 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) $$
Essentially, if a certain property holds for $(a, refl_a)$, then it holds for any $(x, p)$ (where $p$ is evidence that $a = x$, also called a path from $a$ to $x$).
This is also known as path induction.
Again, please note that here $a$ is fixed.
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 $$
Corresponding to the preimage of $b$ under $f$.
Properties of types/functions
is-empty
$$ \text{is-empty}(A) := A → \bot $$
sec/retr
Assuming $f : A → B$, sec denotes the existence of a right inverse for the function.
$$ \text{sec}(f) := \Pi_{(g:B→A)} f ∘ g \sim id $$
retr denotes the existence of a left inverse for the function.
$$ \text{retr}(f) := \Pi_{(h:B→A)} h ∘ f \sim id $$
The reason retr is called retr is that $h$ may only map a subset of B back to A. In this case, we say A is a retraction of B.
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) $$
It is the concept of "bijection" in type theory.
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
- A map is an equivalence if and only if its fibers are contractible
- Observational equal on $ℕ$, $Bool$ and coproduct type, ie. $Eq-ℕ n m$. with one of n and m fixed by $\Sigma$, ie. $\Sigma_{(n:N)} Eq-N(m,n)$
is-coh-invertible
For a function $f : A \rightarrow B$, if it is an equivalence with its inverse being $g$, where the evidence for $g$ being a right inverse is homotopy $G$, and the evidence for $g$ being a left inverse is homotopy $H$, and there exists a homotopy $K : G \cdot f \sim f \cdot H$, we refer to $f$ as a 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\}) $$
It is the concept of "injection" in type theory.
Important embeddings
- For a subtype $B$ of $A$, $\text{is-emb}(proj_1)$ is inhabited, ie. $(a , b) = (a' , b') ≃ a = a'$ where $(a , b)$ and $(a , b) : Σ_{(a : A)} B(a)$
is-surj
$$ \text{is-surj}(f) := \Pi_{(b : B)} ||fib_f(b)|| $$
$\text{is-surj}(f) × \text{is-emb}(f) ↔ is-equiv(f)$
is-prop
$$ \text{is-prop}(A) := \Pi_{(x,y : A)} \text{is-contr}(x = y) $$
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. $Eq-ℕ 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-prop}(A)$ itself 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.
is-subtype
$$ is-subtype(B) := (x : A) → 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.
is-weakly-constant
$$ \text{is-weakly-constant}(f) := (x,y : A) → f(x) = f(y) $$
Universal properties
Coproduct/Disjunction
$$ ((A ∨ B) → X) ≃ ((A + B) → X) ≃ (A → X) \times (B → X) $$
$Σ$ type/Existential
$$ ((∃_{(x:A)} B(x)) → X) ≃ ((Σ_{(x:A)} B(x)) → X) ≃ (\Pi_{(x:A)} (B(x) → X)) $$
or when $B$ does not depend on $A$:
$$ ((A \times B) → X) ≃ (A → (B → X)) $$
Identity type
$$ (\Pi_{(x:A)}(a = x) → B(x)) ≃ B(a) $$
Propositional truncation
$$ (P → Q) ≃ (A → Q) $$
where $P$ and $Q$ are propositions, $f : A → P$ is a propositional truncation of $A$.
Propositional truncation is a functor.
$$ ||–|| : (𝐴 → 𝐵) → (||𝐴|| → ||𝐵||) $$
So here are some examples we have: $$ ||id|| ∼ id $$
$$ ||𝑔 ◦ 𝑓|| ∼ ||𝑔|| ◦ ||𝑓|| $$
$$ ||𝑥 = 𝑦|| ↔ || y = x || $$
$$ || x = y || → || y = z || → || x = z || $$
$$ ||𝐴 × 𝐵|| ≃ ||𝐴|| × ||𝐵|| $$
image
$$ hom_X(i, m) ≃ hom_X(f, m) $$
where $m$ is an embedding.
We say $i$ satisfies the universal property of the image of $f$.
Holds when $f$ is surjective.
surjective map
$$ (\Pi_{(y:B)} P(y)) ≃ (\Pi_{(x:A)} P(f(x))) $$
holds when $f$ is surjective.
embedding + surjective = equivalence
$$ \text{is-surj}(f) × \text{is-emb}(f) ≃ is-equiv(f) $$