Is every projective setoid isomorphic to a type?

Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.

We are going to work in pure Martin-Löf type theory and the straightforward propostions-as-types interpretation of logic, so no univalence, propostional truncation and other goodies are available. Our primary objects of interest are setoids, and Agda's setoids in particular. The content of the post has been formalized in this gist. I am not going to bother to reproduce here the careful tracking of universe levels that the formalization carries out (because it must).

In general, a type, set, or an object X of some sort is said to satisfy choice when every total relation R⊆X×Y has a choice function: (AC)(∀x∈X.∃y∈Y.R(x,y))⇒∃f:X→Y.∀x∈X.R(x,fx). In Agda this is transliterated for a setoid A as follows:

satisfies-choice : ∀ c' ℓ' r → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ' ⊔ suc r)
satisfies-choice c' ℓ' r = ∀ (B : Setoid c' ℓ') (R : SetoidRelation r A B) →
                             (∀ x → Σ (Setoid.Carrier B) (rel R x)) → Σ (A ⟶ B) (λ f → ∀ x → rel R x (f ⟨$⟩ x))

Note the long arrow in A ⟶ B which denotes setoid maps, i.e., the choice map f must respect the setoid equivalence relations ∼A and ∼B.

A category theorist would instead prefer to say that A satisfies choice if every epi e:B→A splits: (PR)(∀B.∀e:B→A.e epi⇒∃s:A→B.e∘s=idA.. Such objects are known as projective. The Agda code for this is

surjective : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ c₂ ⊔ ℓ₂)
surjective {B = B} f = ∀ y → Σ _ (λ x → Setoid._≈_ B (f ⟨$⟩ x) y)

split : ∀ {c₁ ℓ₁ c₂ ℓ₂} {A : Setoid c₁ ℓ₁} {B : Setoid c₂ ℓ₂} → A ⟶ B → Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂)
split {A = A} {B = B} f = Σ (B ⟶ A) (λ g → ∀ y → Setoid._≈_ B (f ⟨$⟩ (g ⟨$⟩ y)) y)

projective : ∀ c' ℓ' → Set (c ⊔ ℓ ⊔ suc c' ⊔ suc ℓ')
projective c' ℓ' = ∀ (B : Setoid c' ℓ') (f : B ⟶ A) → surjective f → split f

(If anyone can advise me how to to avoid the ugly Setoid._≈_ B above using just what is available in the standard library, please do. I know how to introduce my own notation, but why should I?)

Actually, the above code uses surjectivity in place of being epimorphic, so we should verify that the two notions coincide in setoids, which is done in Epimorphism.agda. The human proof goes as follows, where we write =A or just = for the equivalence relation on a setoid A.

Theorem: A setoid morphism f:A→B is epi if, and only if, Π(y:B).Σ(x:A).fx=By.

Proof. (⇒) I wrote up the proof on MathOverflow. That one works for toposes, but is easy to transliterate to setoids, just replace the subobject classifier Ω with the setoid of propositions (Type,↔).

(⇐) Suppose σ:Π(y:B).Σ(x:A).fx=By and g∘f=h∘f for some g,h:B→C. Given any y:B we have g(y)=Cg(f(fst(σy)))=Ch(f(fst(σy)))=Ch(y). QED.

Every type T may be construed as a setoid ΔT=(T,IdT), which is setoid in Agda.

Say that a setoid A has canonical elements when there is a map c:A→A such that x=Ay implies IdA(cx,cy), and cx=Ax for all x:A. In other words, the map c takes each element to a canonical representative of its equivalence class. In Agda:

record canonical-elements : Set (c ⊔ ℓ) where
  field
    canon : Carrier → Carrier
    canon-≈ : ∀ x → canon x ≈ x
    canon-≡ : ∀ x y → x ≈ y → canon x ≡ canon y

Based on my experience with realizability models, I always thought that the following were equivalent:

1. A satisfies choice (AC)
2. A is projective (PR)
3. A is isomorphic to a some ΔT
4. A has canonical elements.

But there is a snag! The implication (2 ⇒ 3) seemingly requires extra conditions that I do not know how to get rid of. Before discussing these, let me just point out that SetoidChoice.agda formalizes (1 ⇔ 2) and (3 ⇒ 4 ⇒ 1) unconditionally. In particular any ΔT is projective.

The implication (2 ⇒ 3) I could prove under the additional assumption that the underlying type of A is an h-set. Let us take a closer look. Suppose (A,=A) is a projective setoid. How could we get a type T such that A≅ΔT? The following construction suggests itself. The setoid map

r:(A,IdA)→(A,=A)r:x↦x

is surjective, therefore epi. Because A is projective, the map splits, so we have a setoid morphism s:(A,=A)→(A,IdA) such that r∘s=id. The endomap s∘r:A→A is a choice of canonical representatives of equivalence classes of (A,=A), so we expect (A,=A) to be isomorphic to ΔT where T=Σ(x:A).IdA(s(rx),x). The mediating isomorphisms are

i:A→Tj:T→Ai:x↦(s(rx),ζx)j:(x,ξ)↦x

where ζx:Id(s(r(s(rx))),s(rx))) is constructed from the proof that s splits r. This almost works! It is easy to verify that j(ix)=Ax, but then I got stuck on showing that IdT(i(j(x,ξ),(x,ξ)), which amounts to inhabiting (1)IdT((x,ζx),(x,ξ)). There is no a priori reason why ζx and ξ would be equal. If A is an h-set then we are done because they will be equal by fiat. But what do to in general? I do not know and I leave you with an open problem:

Is every projective setoids isomorphic to a type?

Egbert Rijke and I spent one tea-time thinking about producing a counter-example by using circles and other HoTT gadgets, but we failed. Just a word of warning: in HoTT/UF the map 1→S1 from the unit type to the circle is onto (in the HoTT sense) but Δ1→ΔS1 is not epi in setoids, because that would split 1→S1.

Here is an obvious try: use the propositional truncation and define T=Σ(x:A).‖IdA(s(rx),x)‖. Now (1) does not pose a problem anymore. However, in order for ΔT to be isomorphic to (A,=A) we will need to know that x=Ay is an h-proposition for all x,y:A.

This is as far as I wish to descend into the setoid hell.