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.

{-# 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.

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.

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.

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.

  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.

  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.

  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.

  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.

  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.

    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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  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.

  ĥ : 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.

  ĥ 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.

  ĥ-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.

  ĥ-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.

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.

    → Σ[ 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.

  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.

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.

  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.

    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.

  ∃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.

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