Families of equivalences

tot function

For a family of maps:

$$ f : \Pi_{(x:A)} B(x) \rightarrow C(x) $$

We define a map $tot$:

$$ tot(f) : \Sigma_{(x:A)} B(x) \rightarrow \Sigma_{(x:A)} C(x) $$ $$ tot(f) := \lambda (x, y). (x , f(x, y)) $$

tot : {A : Set} {B : A → Set} {C : A → Set} → ((x : A) → B x → C x) → (Σ A B → Σ A C)
tot f (x , y) = x , f x y

Given a map $f : A → B$, and a family of maps:

$$ g : \Pi_{(x:A)} C(x) \rightarrow D(f(x)) $$

where C is a type family over A, and D is a type family over B. In this situation, we also say that $g$ is a family of maps over $f$.

Then we define:

$$ tot_f(g) : \Sigma_{(x:A)} {C(x)} → \Pi_{(y:B)} \Sigma_{D(y)} $$

$$ tot_f(g) = λ (x, z). (f(x), g(x, z)) $$

Family of equivalences

We have a family of maps $f : \Pi_{(x:A)} B(x) \rightarrow C(x)$,

if for each $x : A$, $f(x)$ is an equivalence, we say that $f$ is a family of equivalences.

This happens iff $tot(f)$ is an equivalence.

The fundamental theorem

Unary identity system

A (unary) identity system on $A$ at $a$ consists of a type family B over A equipped with $b : B(a)$, such that for any family of types $P(x, y)$ indexed by $x : A$ and $y : B(x)$, the function

$$ h ↦ h(a, b) : \Pi_{(x:A)} \Pi_{(y:B(x))} P(x, y) → P(a, b) $$

has a section.

Fundamental theorem of identity types

Given $a : A$, $x : A ⊢ B(x)$, and

$$ x : A ⊢ f(x) : (a = x) \rightarrow B(x) $$

the following conditions are equivalent:

  1. $ftid : \text{is-contr}(\Sigma_{(x:A)}B(x))$
  2. $ftid(x) : (a = x) ≃ B(x)$
  3. $f(a, refl_a) : B(a)$ is an identity system on A at a
  4. $f(x)$ is an equivalence of types, ie. $x:A \vdash ftid(x) : \text{is-equiv}(f(x))$
  5. $f(x)$ has a section $ftid(x)$, or $f(x)$ is a retraction of $ftid(x)$, ie. $f(x) ∘ ftid(x) \sim id$, where $ftid(x) : B(x) → (a = x)$

Embedding

An embedding is a map $f : A → B$ that satisfies the property that, for every $x, y : A$ $$ ap_f : (x = y) → (f(x) = f(y)) $$ is an equivalence.

We write $\text{is-emb}(f)$ for the type of witnesses that $f$ is an embedding, and we define

$$ A ↪ B := \Sigma_{(f : A → B)} \text{is-emb}(f) $$

In Agda:

is-emb : {A : Set} {B : Set} (f : A → B) → Set
is-emb {A} f = (x y : A) → is-equiv (cong f {x} {y})

_↪_ : {A : Set} {B : Set} → Set → Set → Set
A ↪ B = Σ (A → B) is-emb

Basically, if $is-emb(f)$ is inhabited, then $f$ maps different values in $A$ to different elements in $B$.