quotients and products again

Stream: general

[Reid Barton]

If $(A_i)_{i \in I}$ is a family of sets and $R_i$ is an equivalence relation on $A_i$, then writing $R$ for the product of the relations $R_i$, there is a map $$(\product A_i) / R \to \product (A_i / R_i)$$. Classically this map has an inverse: given an element on the right hand side, we can choose a representative of each factor and assemble them to a representative of a preimage. In mathlib it is implemented here and this has been discussed on Zulip here, here, here and here.

My question today is, can I consider this inverse map to be "constructive"? After all, even though it apparently requires an axiom to define it in Lean, it is also the case that it has a computational interpretation (namely, the identity), because the computational representation of $A/R$ is just that of $A$. Since I don't actually know what it means to be "constructive", maybe a better question is: can this inverse be defined in HoTT without axioms? (Maybe @Floris van Doorn @Ulrik Buchholtz?)

[Reid Barton]

(In HoTT, assume that $A_i$ is a set/0-type and that $A_i/R_i$ is the ordinary set quotient.)

[Reid Barton]

Another thing I don't really understand. Constructively, is there a difference between a quotient map $A \to A/R$ and a general surjective map $A \to B$? The map $A \to A/R$ satisfies "descent", whereas it seems like a general surjection might not. But I don't understand the proof in the HoTT book which claims to prove that the map $A/R \to A//R$ is an isomorphism, where $A//R$ is the set of equivalence classes (Theorem 6.10.6).

[Reid Barton]

Chris keeps bringing up the case where all the relations are the always true relation, so I guess the first question is whether truncation commutes with (infinite) products.

[Reid Barton]

Oh, apparently this is exactly the axiom of choice? I don't know why I find this to be so confusing

[Chris Hughes]

I got confused about the same thing and asked a question here about why you couldn't do choice constructively. I answered it myself. If the domain is a quotient then you get contradictions if you do it the "computable" way.

If you consider the identity function from trunc bool -> trunc bool, and try to make a trunc (trunc bool -> bool) the "computable" way, then you end up with a function defined to be two different things on the same input, i.e. it will not be equal for trunc.mk ff and trunc.mk tt

[Floris van Doorn]

I think saying that the computational interpretation of $A / R$ is $A$ is misleading. Sure, that's how it is implemented in the untrusted evaluator of Lean, but of course you cannot constructively (or even classically) identify them. For example, with this "computational interpretation" you might think we can constructively define a map $A / R \to A$, which of course, we cannot.

Maybe it's helpful to think about how it would be implemented in a cubical type theory, where you have points from $A$, paths from the relation (so point in the context of an interval variable), and then compositions of those paths.

I'm quite sure that requiring an inverse to the map from the quotient-of-products to product-of-quotients is exactly the axiom of choice. To define the map in the other way, you have infinitely many elements in a quotient, and you need a choice function to assume they're all representatives so that you can define a function with them.

[Jeremy Avigad]

I stumbled across exactly this question a little more than a year ago, and, coincidentally, asked some of the local HoTT / DTT people here about a couple of weeks ago.

The principle seems to me to be reasonably constructive, in it is compatible with code extraction (as you say, interpreting the map as the identity function). It is also equivalent to a natural generalization of the lifting property for quotients.

Andrew Swan points out that if you formulate it in the context of HoTT (using HITs for quotients), the principle implies choice. What follows is an email he sent me.

"I had another look at the axiom you asked about today. If I understand it right, then it does entail choice, at least in the presence of propositional truncation and quotients, as they would be defined in HoTT. The main idea is that given a family of types D : A -> Set, we can define B to be the sigma type Σ A D and take the relation R to identify (a, d) and (a', d') when a = a'. Given a term of type Π (a : A) || D a ||, we can get a well defined function g: A -> B/R. Then given an element of (A -> B)/R' in the fibre of g, we can show that there merely exists a choice function for D, i.e. get a term of type || Π (a : A) (D a) ||. It was a good chance to practice my agda, so I did formalised version of the argument."

[Chris Hughes]

The principle seems to me to be reasonably constructive, in it is compatible with code extraction (as you say, interpreting the map as the identity function). It is also equivalent to a natural generalization of the lifting property for quotients.

It's not really compatible with code extraction because interpreting it as the identity is inconsistent. If I make a meta def using quot.unquot to give it the obvious computable interpretation, then I can write a decidable true instance that evaluates to ff.

import data.quot data.setoid

meta def quotient_choice {α β : Type} [s : setoid β]
  (f : α → quotient s) : quotient (@pi_setoid _ _ (λ a : α, s)) :=
quotient.mk (λ a : α, quot.unquot (f a))

--applying choice to the identity map
def decidable_true
  (quotient_choice : Π {α β : Type} [s : setoid β]
    (f : α → quotient s), quotient (@pi_setoid _ _ (λ a : α, s))) :
  decidable true :=
-- ⊤ is the always true relation
by letI : setoid bool := ⊤; exact
quot.rec_on_subsingleton (@quotient_choice (@quotient bool ⊤) bool ⊤ id)
  (λ f, decidable_of_iff (f ⟦ff⟧ = f ⟦tt⟧)
    (iff_true_intro (congr_arg f (quotient.sound trivial))))

#eval decidable_true @quotient_choice --ff

[Gabriel Ebner]

Ah, so the trick is to construct ⟦quot.unquot⟧, then the function quot.unquot ∘ quot.mk is provably constant but implemented as the identity in the VM, which allows you to construct the exotic decidable instance inside the quotient.