{-# OPTIONS --cubical-compatible #-}
module Padova2025.Cubical.Issues.PropositionalTruncation where

Propositional truncation

open import Agda.Primitive
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.EvenOdd
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Termination.Ordering

It is time to confess: What we have defined in the Padova2025.ProvingBasics.Connectives.Existential module as the existential quantifier is not really the existential quantifier from blackboard mathematics, and similarly our disjunction is not really the disjunction from blackboard mathematics.

Our notion of existence is more precisely called “specified existence”, whereas the blackboard’s notion of existence is “mere existence”: According to our definition, a witness of an existential claim is a value of type Σ[ x ∈ A ] B x, so a pair consisting of a specified element x : A and a witness p : B x. So a witness does not only attest that is some element x such that B x; instead, it also explicitly specifies one possible such element x. This is in contrast to the notion of existence from blackboard mathematics, which does not disclose a specified element.

This makes a difference when we use an existential assumption to construct mathematical objects. If the hypothesis is specified existence, the result of our construction may depend on x. If the hypothesis is mere existence, the result is not allowed to depend on x.

In the following, we will write mere existence as ∥ Σ[ x ∈ A ] B x ∥ (keeping in mind that standard Agda does not support this).

Propositions as some types

We can make this more precise by introducing the term proposition for those types whose values are all equal:

isProp : {ℓ : Level} → Set ℓ → Set ℓ
isProp X = (a b : X) → a ≡ b

For a type satisfying isProp, the only interesting question is whether it is inhabited.

For instance, for every number n, the type Even n of witnesses that n is even is a proposition:

Even-isProp : (n : ℕ) → isProp (Even n)
Even-isProp = {!!}

In contrast, the type Σ[ x ∈ A ] B x is typically not a proposition.

Elimination principles

For specified existence, we have the following elimination principle: “If, given an element x : A and a witness p : B x, we have a way of constructing an element of type R, then we also have a way of constructing such an element from the assumption Σ[ x ∈ A ] B x.”

Σ-elim : {A : Set} {B : A → Set} {R : Set} → ((x : A) → B x → R) → (Σ[ x ∈ A ] B x → R)
Σ-elim = {!!}

For mere existence, which standard Agda does not have, we only have the following weaker principle:

mere-existence-elim : {A : Set} {B : A → Set} {R : Set} → isProp R → ((x : A) → B x → R) → (∥ Σ[ x ∈ A ] B x ∥ → R)

In contrast to Σ-elim, the elimination principle for mere existence requires the result type R to be a proposition.

A fine point for both kinds of existence, not expressed in the type signatures of Σ-elim and the (fictitious, in standard Agda) mere-existence-elim above, is that the result type R does not need to belong to the base universe Set. It could also be a larger type, living in Set₁, Set₂ or beyond.

The axiom of choice?

The difference between the two notions of existence is especially visible in the interaction with functions. For instance, the following statement looks a bit like the axiom of choice—well-known as a cornerstone of classical foundations of mathematics. One would therefore not expect it to be provable in standard Agda, which is constructive by default. And yet it is:

kinda-looking-like-the-axiom-of-choice
  : {A B : Set} {R : A → B → Set}
  → ((x : A) → Σ[ y ∈ B ] R x y)
  → Σ[ f ∈ (A → B) ] ((x : A) → R x (f x))
kinda-looking-like-the-axiom-of-choice = {!!}

With our definitions, a witness of a statement “∀x:A. ∃y:B. R x y” is already a function inputting an element x : A and outputting a pair consisting of a suitable element y : B and a witness of R x y. Transforming such a witness into a choice function is just a matter of repackaging the provided information; formulated with specified existence instead of mere existence, choice is not a principle with far-reaching consequences, but simply a constructive tautology.

An impredicative fallback

Cubical Agda will allow us, for every type A : Set, to construct its propositional truncation ∥ A ∥ : Set, the reflection of A in the world of propositions. The construction will look like this:

-- a "higher inductive type"; only available in cubical mode
data ∥_∥ (A : Set) : Set where
  ∣_∣    : A → ∥ A ∥
  squash : (x y : ∥ A ∥) → x ≡ y

So the truncation ∥ A ∥ will be like A, but with extra identifications, forcing ∥ A ∥ to be a proposition. It can be pictured as the quotient of A by the equivalence relation which deems any two elements equivalent.

In standard Agda, we can approximate propositional truncation by an impredicative encoding—at the price of having to jump to the next universe level.

-- impredicative fallback to true propositional truncation in standard Agda
∥_∥ : Set → Set₁
∥ A ∥ = ({R : Set} → isProp R → (A → R) → R)

This approximation validates the desired elimination principle by definition, though only for result types R which live in the base universe Set:

∥∥-elim : {A : Set} {R : Set} → isProp R → (A → R) → (∥ A ∥ → R)
∥∥-elim = {!!}

Cubical Agda’s definition of propositional truncation as a higher inductive type would support the following stronger principle:

-- referring to the true ∥_∥, not the impredicative approximation
∥∥-elim : {ℓ : Level} {A : Set} {R : Set ℓ} → isProp R → (A → R) → (∥ A ∥ → R)

The impredicative approximation to the true propositional truncation is definitely useful, though the restricted elimination principle is a serious limitation, especially in view since the truncation itself does not live in the base universe; nested applications of our approximation will run into issues.

Another (quite embarrassing) deficiency of our approximation to propositional truncation is that it fails to produce a proposition. Function extensionality would be required for isProp (∥ A ∥).

Specified existence from mere existence

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Operators
open import Padova2025.ProvingBasics.Connectives.More
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Negation

In general, we cannot deduce specified existence of an element x : A such that B x from mere existence of such an element; specified existence is much stronger. But in some exceptional situations we can explicitly reconstruct a witness x from the mere knowledge that one exists. Let us explore one such situation here.

The decidable case

As a warmup, let us show ∥ A ∥ → A when A is decidable.

decidable-escape : {A : Set} → Dec A → ∥ A ∥ → A
decidable-escape = {!!}

Roots of functions

A root of a function f : ℕ → Bool is a number n such that f n ≡ false. From mere existence of a root x we can find, by checking each number up to x in turn, the minimal root. Unlike an arbitrary root, the minimal root is unique; this is what allows us to go from mere existence to specified existence.

TODO

Anonymous existence

In addition to specified existence and mere existence, there is also doubly negated existence, sometimes called anonymous existence or classical existence. (But be aware that “anonymous existence” also sometimes refers to mere existence.)

Among these three, anonymous existence is the weakest notion. A value of type ¬ ¬ (Σ[ x ∈ A ] B x) is just a witness that it is impossible that no x with B x exists. Such a witness promises that such an element exists (somewhere, in the platonic heaven?) without revealing any way to find it.

∥∥→¬¬ : {A : Set} → ∥ A ∥ → ¬ ¬ A
∥∥→¬¬ = {!!}