把 `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*
```