Zulip Chat Archive

Stream: general

Topic: quotients and products again

Reid Barton (Feb 03 2020 at 23:51):

If (Ai)iI(A_i)_{i \in I} is a family of sets and RiR_i is an equivalence relation on AiA_i, then writing RR for the product of the relations RiR_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/RA/R is just that of AA. 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 (Feb 03 2020 at 23:52):

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

Reid Barton (Feb 04 2020 at 00:08):

Another thing I don't really understand. Constructively, is there a difference between a quotient map AA/RA \to A/R and a general surjective map ABA \to B? The map AA/RA \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/RA//RA/R \to A//R is an isomorphism, where A//RA//R is the set of equivalence classes (Theorem 6.10.6).

Reid Barton (Feb 04 2020 at 00:14):

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 (Feb 04 2020 at 00:19):

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

Chris Hughes (Feb 04 2020 at 00:32):

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 (Feb 04 2020 at 06:30):

I think saying that the computational interpretation of A/RA / R is AA 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/RAA / 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 AA, 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 (Feb 06 2020 at 20:07):

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 (Feb 07 2020 at 05:08):

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 (Feb 07 2020 at 08:54):

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.

Last updated: Dec 20 2023 at 11:08 UTC