---
title: "Cantor–Schröder–Bernstein for small presentations"
module: V.CantorBernstein
lang: en
site: "Bedrock"
description: "Cantor–Schröder–Bernstein for small presentations"
stage: "Ordinals, injections and cardinals"
reading_order: 93
canonical: https://bedrock.institute/en/V.CantorBernstein.html
html: V.CantorBernstein.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/CantorBernstein.lagda.md
prerequisites: [Base.Prelude, Base.Classical]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/V.CantorBernstein.md, https://bedrock.institute/ja/V.CantorBernstein.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Cantor–Schröder–Bernstein for small presentations

Mutual injections between the small presentations of two sets determine a bijection. The proof first constructs the bijection for small types under excluded middle, then gives a generic form that turns any mutually available coded injections into such a bijection.

The classical Cantor–Schröder–Bernstein theorem says that injections $f : A → B$ and $g : B → A$ yield a bijection $A → B$. In this chapter the two types share one universe level ℓ, and the only extra assumption is excluded middle at that level: for every proposition living at level ℓ, a proof or a refutation. The argument itself belongs to the index types $A$ and $B$, not to the sets of the cumulative hierarchy, which is precisely what later lets it be replayed on the member types of arbitrary small presentations. The proof needs to form some propositions by truncation and then to decide them; the setup below therefore fixes both the classical hypothesis and the proposition-valued vocabulary it will be applied to.

A decision at level ℓ is packaged once and reused throughout: `LEM ℓ` takes a proposition `P : hProp ℓ` and returns either a proof of `⟨ P ⟩` or a refutation, a map from `⟨ P ⟩` into the empty type. The module parameter `lem` is therefore an instance at this one level, not a global principle for all levels. Everything constructed in the chapter will be parametric in it, so the hypothesis appears explicitly wherever a classical verdict is consumed.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module V.CantorBernstein {ℓ : Level} (lem : LEM ℓ) where

open import Cubical.Functions.Embedding using ( Embedding-into-isSet→isSet )
```

The proof will form several propositions by truncating an existential: the statement that x lies in the image of g is ∥ Σ[ y ∈ B ] (g y ≡ x) ∥₁, which is merely inhabited rather than carrying a chosen preimage. Such truncated statements are propositions by `squash₁`, and a proof of one cannot be eliminated into arbitrary data, only into a proposition-valued target. That restriction is exactly why the classical hypothesis will be needed: to turn a mere existence into a chosen preimage when the argument requires one.

```agda
import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
import Cubical.HITs.PropositionalTruncation as PT
```

Two kinds of propositions dominate the chapter: membership in the image of g, and reachability by a finite alternating chain. Both are stored as elements of `hProp ℓ`, which packages an underlying type with a proof that it is a proposition; `⟨ P ⟩` projects the underlying type, while the propositionhood proof stays in the second component. The remaining imports supply the machinery around them: disjoint sums for the bad/good case split, `isProp⊥` for the refutation side, `Σ≡Prop` for identifying pairs whose second components are proposition-valued, and the cumulative hierarchy together with the fact that a member type `⟪ a ⟫` of a set embeds into an h-set, which will later certify that the member types are h-sets.

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ )
```

Two injections, one each way, give one bijection. This section proves that for two types $A$ and $B$ at the same universe level, with $A$ an h-set, under excluded middle at that level. The construction classifies each element of $A$ as bad or good: the bad elements are those reachable by a finite alternating preimage chain that starts outside the image of $g$. A bad element is sent forward through $f$, a good element back along a chosen inverse of $g$. Excluded middle enters twice, once to decide the badness proposition `C` and once to extract a chosen preimage from the truncated image statement; the chain itself is the predicate family `Cₙ`, and the only structural fact it needs is that $x ↦ g (f x)$ preserves badness.

The construction is packaged in a module `Bernstein` taking exactly the classical data: the two types, the h-set structure of $A$, and the two injections, each given as a function together with its injectivity proof. Its first ingredient is the image predicate `imG x`, which asserts merely that some $y ∈ B$ satisfies $g y ≡ x$. No preimage is chosen here; the truncation ∥ ⋯ ∥₁ erases the witness and leaves a proposition, and `squash₁` is the certificate of that propositionhood.

```agda
module Bernstein {A B : Type ℓ} (setA : isSet A)
                 (f : A → B) (fi : (x y : A) → f x ≡ f y → x ≡ y)
                 (g : B → A) (gi : (x y : B) → g x ≡ g y → x ≡ y) where

  imG : A → hProp ℓ
  imG x = (∥ Σ[ y ∈ B ] (g y ≡ x) ∥₁ , squash₁)
```

The base of the badness hierarchy says that x is bad at level zero when it is not in the image of g at all. Since a refutation of `imG x` is a map from `⟨ imG x ⟩` into the empty type, `C₀ x` is a function type, and it is a proposition because a function into a proposition is one. The step `C₊ C x` then says that x is reachable from a bad element by one backward step: merely there are $y ∈ B$ and $z ∈ A$ with $g y ≡ x$, $f z ≡ y$, and z already bad for C. Applying this operator iteratively from `C₀` gives `Cₙ`, so an inhabitant of `Cₙ n x` records an alternating chain x = g y, y = f z, z bad one level down, of length n.

```agda
  C₀ : A → hProp ℓ
  C₀ x = ((⟨ imG x ⟩ → Empty.⊥) , isPropΠ (λ _ → isProp⊥))

  C₊ : (A → hProp ℓ) → A → hProp ℓ
  C₊ C x = (∥ Σ[ y ∈ B ] Σ[ z ∈ A ] ((g y ≡ x) × ((f z ≡ y) × ⟨ C z ⟩)) ∥₁ , squash₁)

  Cₙ : ℕ → A → hProp ℓ
```

The two defining equations of `Cₙ` are computation rules: at index zero it is the base predicate, at the successor it applies the step once. The full badness proposition `C x` then truncates over all chain lengths at once: x is bad when merely some `Cₙ n x` holds. The truncation is essential here, since it collapses the infinitely many levels of the hierarchy into a single proposition at which excluded middle can later be applied.

```agda
  Cₙ zero = C₀
  Cₙ (suc n) = C₊ (Cₙ n)

  C : A → hProp ℓ
  C x = (∥ Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ ∥₁ , squash₁)
```

Before using the hierarchy, one small bookkeeping lemma is recorded: a badness proof at any fixed level n yields a badness proof. Its content is simply that the pair (n , proof) is a witness for the truncated existential defining `C`, and ∣ ⋯ ∣₁ injects that witness into the truncation. Every later argument that produces a chain of some length will pass through this map.

```agda
  c-in : {x : A} {n : ℕ} → ⟨ Cₙ n x ⟩ → ⟨ C x ⟩
  c-in {x} {n} h = ∣ n , h ∣₁
```

The one structural fact promised in the lead is now proved: if x is bad, so is g (f x). Given a chain of length n ending at x, one extends it by a single backward step, since x itself serves as the element z and f x as the element y: the required paths g (f x) ≡ g (f x) and f x ≡ f x are both reflexivity, and the old chain is the tail. The result is a chain of length suc n ending at g (f x). Because the input is truncated, the elimination `PT.rec` targets the propositionhood of the output, which is legitimate since `C (g (f x))` is a proposition.

```agda
  gf-closed : {x : A} → ⟨ C x ⟩ → ⟨ C (g (f x)) ⟩
  gf-closed {x} = PT.rec (snd (C (g (f x)))) go
    where
    go : Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ → ⟨ C (g (f x)) ⟩
    go (n , cx) = c-in {x = g (f x)} {n = suc n} ∣ f x , x , (refl , (refl , cx)) ∣₁
```

Closure under g ∘ f tells us badness propagates forward, but to route elements through h we also need to look one level backward: every badness proof either bottoms out at level zero, or x is of the form g (f z) with z bad. This is exactly what `C-view` delivers. The target is itself truncated, so eliminating into it is unproblematic even though the case analysis on the chain length n is genuine data.

```agda
  C-view : {x : A} → ⟨ C x ⟩
         → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
  C-view {x} = PT.rec squash₁ go
    where
```

The proof splits on the recorded length. At length zero the chain simply asserts that x is outside the image of g, which is the left disjunct verbatim. At length suc n the stored witness is a triple y, z with g y ≡ x, f z ≡ y and a length-n badness proof for z; composing the two paths by way of g gives g (f z) ≡ x, and the shorter chain is included with `c-in`. The right disjunct is exactly the pair (z , that path , that shorter proof), truncated. This lemma is the surjectivity engine later: applied at g y, it either refutes badness outright or produces the preimage z.

```agda
    go : Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
    go (zero , c0) = ∣ inl c0 ∣₁
    go (suc n , cs) = PT.map inr (PT.map (λ { (y , z , gy , fz , cz) →
        z , ((cong g fz ∙ gy) , c-in {x = z} {n = n} cz) }) cs)
```

The second use of excluded middle converts goodness into image membership. Suppose x is good, in the strong sense that `C x` admits a refutation. Deciding the proposition `imG x` gives either a preimage, which is what we want, or a refutation of image membership, that is, a proof of `C₀ x`. But level zero implies badness via `c-in`, contradicting the assumed refutation of `C x`; from that contradiction anything follows. So `notC→imG` produces an inhabitant of `⟨ imG x ⟩`, still merely, not yet a chosen preimage.

```agda
  notC→imG : {x : A} → (⟨ C x ⟩ → Empty.⊥) → ⟨ imG x ⟩
  notC→imG {x} nC = Sum.rec {A = ⟨ imG x ⟩} {B = ⟨ imG x ⟩ → Empty.⊥} {C = ⟨ imG x ⟩}
    (λ h → h) (λ nC₀ → Empty.rec (nC (c-in {n = zero} nC₀)))
    (lem (imG x))
```

To turn the mere image membership into a chosen preimage, we may eliminate the truncation into the fiber type Σ[ y ∈ B ] (g y ≡ x) itself, provided that type is a proposition. This is where the hypotheses on g and A earn their keep: injectivity of g shows any two preimages y and y' are equal, using the paths p and p' to g x, and the h-set structure of A makes the resulting equality in A a proposition, which `Σ≡Prop` then extends to the whole pair. Note that the h-set assumption is needed exactly here and nowhere else in the construction.

```agda
  fiberG-prop : (x : A) → isProp (Σ[ y ∈ B ] (g y ≡ x))
  fiberG-prop x (y , p) (y' , p') = Σ≡Prop {A = B} {B = λ y → g y ≡ x}
    (λ y → setA (g y) x) (gi y y' (p ∙ sym p'))
```

With fiber propositionhood in hand, `fiberG` is the elimination of the truncated image statement into the fiber type: since the target is a proposition, `PT.rec` applies with the identity on fibers as the action. This is the first point in the argument where a chosen preimage exists as data rather than merely, and it was unlocked by excluded middle plus the h-set structure, not by any property of the truncation alone.

```agda
  fiberG : (x : A) → ⟨ imG x ⟩ → Σ[ y ∈ B ] (g y ≡ x)
  fiberG x = PT.rec (fiberG-prop x) (λ w → w)
```

For a good element x, the chosen preimage can now be named `ginv x`: it is the first component of the fiber produced by `fiberG` from `notC→imG`. Its spec `ginv-spec` records that g (ginv x) ≡ x, taken from the second component of the same fiber. So on the good side the map h will send x back to a point of B whose g-image is exactly x, as an inverse segment of g deserves.

```agda
  ginv : {x : A} → (⟨ C x ⟩ → Empty.⊥) → B
  ginv {x} nC = fiberG x (notC→imG nC) .fst

  ginv-spec : {x : A} (nC : ⟨ C x ⟩ → Empty.⊥) → g (ginv nC) ≡ x
  ginv-spec {x} nC = fiberG x (notC→imG nC) .snd
```

The candidate bijection h is now defined on a hypothetical verdict rather than on A directly: given x and a decision d of the badness proposition `C x`, it sends x to f x in the bad case and to `ginv x` in the good case. Working with the verdict as an explicit argument keeps the case analysis honest, and the two lemmas that follow, injectivity and surjectivity relative to a verdict, will be combined with the actual decision supplied by `lem` at the end of the section.

```agda
  h : (x : A) → ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) → B
  h x (inl _) = f x
  h x (inr nC) = ginv nC
```

Injectivity of h is proved by four cases on the pair of verdicts. When both sides are bad, h is f on both, and the injectivity of f finishes immediately. When x is bad and x' good, the hypothesis h x dx ≡ h x' dx' says g (f x) ≡ ginv x', hence g (g (f x)) ≡ x' after applying g and the spec of ginv. Since badness propagates along g ∘ f, x bad makes g (f x) bad; transporting the badness of g (f x) along that path with `subst` makes x' bad, contradicting the verdict that x' is good.

```agda
  h-inj : (x x' : A) (dx : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) (dx' : ⟨ C x' ⟩ ⊎ (⟨ C x' ⟩ → Empty.⊥))
        → h x dx ≡ h x' dx' → x ≡ x'
  h-inj x x' (inl cx) (inl cx') e = fi x x' e
  h-inj x x' (inl cx) (inr nCx') e =
    Empty.rec (nCx' (subst (λ w → ⟨ C w ⟩) (cong g e ∙ ginv-spec nCx') (gf-closed {x = x} cx)))
```

The mirror case, x good and x' bad, is symmetric: the transport runs along the reversed path and kills x instead. In the final case both sides are good, so h is ginv on both and the equation reads ginv x ≡ ginv x'. Applying g turns it into g (ginv x) ≡ g (ginv x'), and chaining the two specs of ginv around it yields x ≡ x' directly. No h-set assumption is used anywhere in this lemma; injectivity is pure case analysis on verdicts.

```agda
  h-inj x x' (inr nCx) (inl cx') e =
    Empty.rec (nCx (subst (λ w → ⟨ C w ⟩) (sym (cong g e) ∙ ginv-spec nCx) (gf-closed {x = x'} cx')))
  h-inj x x' (inr nCx) (inr nCx') e = sym (ginv-spec nCx) ∙ cong g e ∙ ginv-spec nCx'
```

Surjectivity relative to a verdict is stated for each y ∈ B, with the verdict taken on the element g y of A rather than on an element of B. In the good case the preimage is simply g y itself: it is good by assumption, h sends it to `ginv (g y)`, and the spec of ginv together with injectivity of g identifies that value with y. The witness is packaged as a truncated pair since the final theorem only claims mere surjectivity.

```agda
  h-surj : (y : B) (d : ⟨ C (g y) ⟩ ⊎ (⟨ C (g y) ⟩ → Empty.⊥))
         → ∥ Σ[ x ∈ A ] Σ[ dx ∈ ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) ] (h x dx ≡ y) ∥₁
  h-surj y (inr nCgy) = ∣ g y , inr nCgy , gi (ginv nCgy) y (ginv-spec nCgy) ∣₁
```

In the bad case for g y, `C-view` decomposes the badness proof into two alternatives. The first says g y is outside the image of g, but y itself witnesses its image membership with the path reflexivity, a contradiction that yields anything, in particular the required truncated statement. The second produces z ∈ A with g (f z) ≡ g y and z bad; then z is a preimage, for h z = f z and g (f z) equals g y, so injectivity of g identifies f z with y. Both branches exhibit their witnesses inside one truncation, so no verdict other than the one already assumed is consumed.

```agda
  h-surj y (inl cgy) = PT.rec squash₁
    (λ { (inl c0) → Empty.rec (c0 ∣ y , refl ∣₁) ; (inr (z , gfy , cz)) → ∣ z , inl cz , gi (f z) y gfy ∣₁ })
    (C-view {x = g y} cgy)
```

The final lemma answers an objection to the whole design: h was defined relative to a verdict, yet the theorem needs a single function on A. `h-cons` says the choice of verdict does not matter, for any fixed x the two outputs are equal. Both bad gives reflexivity, either mixed case is contradictory since one verdict refutes the other's witness, and both good reduces to the uniqueness of the chosen preimage: the two fibers produced by `fiberG` are equal because the fiber type is a proposition, and taking first components preserves that equality by congruence. This consistency is what makes the verdict-dependent construction a genuine definition of a map.

```agda
  h-cons : (x : A) (dx dx' : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) → h x dx ≡ h x dx'
  h-cons x (inl cx) (inl cx') = refl
  h-cons x (inl cx) (inr nCx') = Empty.rec (nCx' cx)
  h-cons x (inr nCx) (inl cx) = Empty.rec (nCx cx)
  h-cons x (inr nCx) (inr nCx') = cong fst (fiberG-prop x (fiberG x (notC→imG nCx)) (fiberG x (notC→imG nCx')))
```

With consistency established, the verdict can be fed in once and for all. The next three lines assemble the theorem.

```agda
  ĥ : A → B
```

The map `ĥ` is h applied to the canonical verdict `lem (C x)`: excluded middle decides the badness of each x, and h-cons guarantees that any other decision would have produced the same value. This is where the module's hypothesis `lem` is consumed for the definition itself.

```agda
  ĥ x = h x (lem (C x))
```

Injectivity transfers verbatim from the relative version, since the canonical verdicts are particular choices of the verdict arguments: `ĥ-inj x x' e` is exactly `h-inj` at those verdicts.

```agda
  ĥ-inj : (x x' : A) → ĥ x ≡ ĥ x' → x ≡ x'
  ĥ-inj x x' e = h-inj x x' (lem (C x)) (lem (C x')) e
```

Surjectivity needs one extra step. The relative lemma `h-surj` applied at the canonical verdict for g y provides a truncated triple x, dx, and a path h x dx ≡ y, but its first two components speak about the hypothetical h x dx rather than `ĥ x`. Rewriting along `h-cons x dx (lem (C x))`, which identifies the two values, and prepending the symmetric path converts the triple into a witness of `ĥ x ≡ y`. The whole statement remains truncated: the theorem asserts that a preimage merely exists.

```agda
  ĥ-surj : (y : B) → ∥ Σ[ x ∈ A ] (ĥ x ≡ y) ∥₁
  ĥ-surj y = PT.map (λ { (x , dx , e) → x , sym (h-cons x dx (lem (C x))) ∙ e })
    (h-surj y (lem (C (g y))))
```

The abstract construction now applies to the cumulative hierarchy itself. Each element a of V comes with a member type ⟪ a ⟫, the type of its members. The Bernstein construction asks for an h-set structure on its first type, so the first step is to certify that ⟪ a ⟫ is one. The embedding ⟪ a ⟫↪ sends each member index to the member it indexes inside V; since V is an h-set and the embedding is an embedding, its domain inherits the h-set condition. With that single fact, two mutual injections between ⟪ a ⟫ and ⟪ b ⟫ produce a bijection packaged as a dependent triple.

The h-set certificate composes two imported facts. The map ⟪ a ⟫↪ is an embedding into V, meaning all its fibers are propositions, and the hierarchy V is an h-set by its constructor setIsSet. A type that embeds into an h-set is itself an h-set, since equality in the domain can be compared after applying the embedding. The signature that follows then states the set-theoretic corollary in the same shape as the abstract theorem: injections f from ⟪ a ⟫ to ⟪ b ⟫ and g back, each with its injectivity proof, taken as explicit hypotheses.

```agda
small-set : (a : V ℓ) → isSet (⟪ a ⟫)
small-set a = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet

cantor-bernstein : (a b : V ℓ) (f : ⟪ a ⟫ → ⟪ b ⟫)
    → ((x y : ⟪ a ⟫) → f x ≡ f y → x ≡ y)
    → (g : ⟪ b ⟫ → ⟪ a ⟫) → ((x y : ⟪ b ⟫) → g x ≡ g y → x ≡ y)
```

The result type is an explicit dependent triple rather than a record: a function h from ⟪ a ⟫ to ⟪ b ⟫, its injectivity as a proposition-valued component, and mere surjectivity, asserting for each y of ⟪ b ⟫ a truncated preimage. The asymmetry between the two side conditions is deliberate and mirrors the abstract theorem: injectivity is stated as honest data, surjectivity only as mere existence. Nothing in the statement quantifies over stages or membership of the hierarchy; everything happens inside the two member types.

```agda
    → Σ[ h ∈ (⟪ a ⟫ → ⟪ b ⟫) ]
        (((x y : ⟪ a ⟫) → h x ≡ h y → x ≡ y)
      × ((y : ⟪ b ⟫) → ∥ Σ[ x ∈ ⟪ a ⟫ ] (h x ≡ y) ∥₁))
cantor-bernstein a b f fi g gi = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )
  where
```

The proof is a single instantiation. Instantiating the module `Bernstein` at A = ⟪ a ⟫ and B = ⟪ b ⟫, with the h-set certificate supplied for A and the two injections passed through unchanged, exposes the components ĥ, ĥ-inj and ĥ-surj; the definition assembles them into the triple. All the work of the previous section is reused without modification.

```agda
  module M = Bernstein {A = ⟪ a ⟫} {B = ⟪ b ⟫} (small-set a) f fi g gi
```

The corollary above hard-wires the member types of V. A more reusable form keeps the setting abstract: a carrier `C` of codes, an assignment `P` of a small type to each code, and a relation `R a b` expressing that a codes an injection from P a to P b. What ties the abstraction to the previous section is the readback `read`: from an inhabitant of R a b it extracts an actual function together with its injectivity proof. Given one such readback in each direction, the Bernstein construction applies verbatim. Two entry points are provided, one taking the pair of coded injections as data and one taking it merely, with the bijection then merely existing as well.

The parameters spell out the exact strength required. The carrier C lives at its own level ℓ₁ and the relation R at ℓ₂, so codes and their relations need not be small; what must be small is each P a, at the fixed level ℓ where excluded middle is available. For every a, P a is assumed an h-set, mirroring the h-set hypothesis of the Bernstein module. The relation R itself is left completely arbitrary as a type: nothing about it is assumed beyond the readback, which from an inhabitant of R a b returns a pair whose first component is a function P a → P b and whose second is that function's injectivity proof. In particular, the extracted injection is honest data, not a truncated existence.

```agda
module MutualInj {ℓ₁ ℓ₂ : Level} (C : Type ℓ₁) (P : C → Type ℓ)
    (R : (a b : C) → Type ℓ₂)
    (setP : (a : C) → isSet (P a))
    (read : (a b : C) → R a b
          → Σ[ f ∈ (P a → P b) ] ((x y : P a) → f x ≡ f y → x ≡ y)) where
```

The first entry point states the transfer with the two coded injections as explicit arguments: from a forward code in R a b and a backward code in R b a, it returns the bijection between P a and P b as a triple, in exactly the shape of the previous section. The statement quantifies over inhabitants of the relation, not over their truncation, so the codes are available as data throughout.

```agda
  mutual→bijection : (a b : C) → R a b → R b a
    → Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁))
  mutual→bijection a b fwd bwd = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )
```

The definition instantiates the Bernstein module at A = P a and B = P b, and this is where the readback is spent. The forward code fwd is unpacked by `read a b` into its function and injectivity components, and the backward code likewise with the arguments of R and read reversed; each projection is selected with the first and second component accessors. The h-set field receives `setP a`. What reaches the Bernstein module are therefore genuine injections, and everything proved there applies unchanged.

```agda
    where
    module M = Bernstein {A = P a} {B = P b} (setP a)
      (read a b fwd .fst) (read a b fwd .snd)
      (read b a bwd .fst) (read b a bwd .snd)
```

The second entry point weakens the input to mere existence: instead of codes, it receives truncated statements that such codes merely exist. Its conclusion is correspondingly weakened twice. The bijection statement itself is truncated, and surjectivity was already truncated inside; so the final type asserts that a bijection merely exists, not that any particular one can be named. Weakening is irreversible here: the truncation on the input cannot be eliminated into the data of a bijection, only into a proposition-valued target, which the whole statement is.

```agda
  ∃bijection : (a b : C) → ∥ R a b ∥₁ → ∥ R b a ∥₁
    → ∥ Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁)) ∥₁
  ∃bijection a b fwd bwd = PT.rec squash₁
```

The proof nests two truncation eliminations. Eliminating fwd yields some code w; eliminating bwd yields w'; the target of the inner elimination is the truncation of the whole bijection statement, which is a proposition by squash₁, so producing the explicit triple from `mutual→bijection` and injecting it with ∣ ⋯ ∣₁ is legitimate. The order of the two eliminations is immaterial, as both targets are propositions.

```agda
    (λ w → PT.rec squash₁ (λ w' → ∣ mutual→bijection a b w w' ∣₁) bwd)
    fwd
```