`e` の順写像を `c` と名付ける。すると `c P` が `Ω` における `P` の符号になる。
```agda
c : hProp ℓ₁ → Ω
c = equivFun e
```
**構成** (`codedTruth`) 符号 `c P` は `Ω` の一点である。命題を得るには、それが真の命題の符号と等しいかを問えばよい：`c ⊤ ≡ c P`。このパス型はレベル `ℓ₂` に属する。`e` が `hProp ℓ₁` の h-集合構造を `Ω` へ運ぶので、これは命題である。これを `P` の代表とし、以下の同型によって真理内容が等しいことを確かめる。
```agda
codedTruth : hProp ℓ₁ → hProp ℓ₂
codedTruth P = (c ⊤ ≡ c P) , isOfHLevelRespectEquiv 2 e isSetHProp _ _
```
`Ω` の帯状領域は、端点を `c(⊤)`、`c(P)` とするパスの族を表す。クリックすると、この族が第二の型の空間へ広がり、パス全体がその点として描かれる。図の `q`、`r` は `P` の証明を前提とするが、`⟨ P ⟩` との型同値そのものにはこの仮定は不要である。
$$\langle P\rangle$$
$$: \operatorname{Type}_{\ell_1}$$
$p$
$\simeq$
$$\langle\operatorname{codedTruth}\,P\rangle$$
$$: \operatorname{Type}_{\ell_2}$$
$q$
$r$
$$\Omega$$
$$: \operatorname{Type}_{\ell_2}$$
$q$
$\langle\operatorname{codedTruth}\,P\rangle$
$r$
$c(\top)$
$c(P)$
`⟨ codedTruth P ⟩` の一点は、`Ω` の一本のパスそのものである：`⟨ codedTruth P ⟩ = (c(⊤) ≡ c(P))`。二つの証明の型はそれぞれレベル `ℓ₁` と `ℓ₂` に属し、互いに型同値である
**補題** (`codedTruthIso`) `P` の基礎型は `codedTruth P` の基礎型と同型である。したがって、上で構成した代表は確かに `P` と同じ真理内容をもつ。
```agda
codedTruthIso : (P : hProp ℓ₁) → Iso ⟨ P ⟩ ⟨ codedTruth P ⟩
```
**証明** 二方向の写像 `to` と `from` を構成し、`iso` でまとめる。始域 `⟨ P ⟩` と終域 `⟨ codedTruth P ⟩` はどちらも命題なので、二つの写像を与えれば、両端の命題性が二つの往復則を直接証明する。写像が真の命題の要素を返す箇所では、その唯一の要素 `tt*` を明示する。
```agda
codedTruthIso P = iso to from (λ q → ⟨ codedTruth P ⟩isProp _ q) (λ p → ⟨ P ⟩isProp _ p)
where
```
あとは二方向の写像を構成する。
- `to` では、証明 `p : ⟨ P ⟩` によって `⊤` と `P` が論理的同値になる。命題外延性からパス `⊤ ≡ P` を得て、`cong c` によって `c ⊤ ≡ c P`、すなわち `codedTruth P` の証明を得る。
```agda
to : ⟨ P ⟩ → ⟨ codedTruth P ⟩
to p = cong c (⇔toPath (λ _ → p) (λ _ → tt*))
```
- `from` では、`q : c ⊤ ≡ c P` から出発する。型同値 `congEquiv e` は命題間のパスと符号間のパスを結ぶ。その逆写像 `invEq (congEquiv e)` によって `⊤ ≡ P` を復元し、`subst ⟨_⟩` でこのパスに沿って `tt*` を輸送すれば、`P` の証明が得られる。
```agda
from : ⟨ codedTruth P ⟩ → ⟨ P ⟩
from q = subst ⟨_⟩ (invEq (congEquiv e) q) tt*
```