is subobject classifier of setoids constructive?

[HuStmpHrrr]

I am trying to show setoids are a topos except that I have trouble constructing a subobject classifier. during the proof, it involves to construct h : Y => 2, given an injection f : X => Y, where h(y) = 1 only when y is in the image of f. This sounds Choice to me.

Or can we have an alternative definition of subobject classifier so that this is constructive?

[JacquesCarette]

The problem is that, constructively, the subterminal objects are not provably equivalent to 2 - you need excluded middle for that (to prove that subterminals are either inhabited or not). I'm pretty sure that the 'set' of subterminal objects is a Setoid, so that would be one place to start. The 'true' morphism would then give you an actual inhabitant.

[JacquesCarette]

The 'answer' seems to be in Setoids in Type Theory, which I was just reading last night! Lemma 36. Omega is the Setoid of Prop. And that seems to need Choice.

[JacquesCarette]

I'm pretty sure a better answer is in these slides, slide 18 in particular. The difference is that Prop is proof irrelevant, and the slides are in a proof-relevant situation. In other words, it (and the web site https://github.com/brunjlar/protop) claim that the key is 'in the proofs'.

On the other hand, Benno van den Berg's PhD Thesis makes me doubt this again!

[HuStmpHrrr]

I don't quite understand how the slides handle omega in haskell. is the proof-relevance there even crazier, with effects even on the proofs?

[TOTBWF]

The issue isn't so much picking Ω, but defining the classifying map. Consider the following definition:

Setoids-SubobjectClassifier : ∀ c → SubobjectClassifier (Setoids (suc c) (suc c))
Setoids-SubobjectClassifier c = record
  { Ω = ≅-setoid (liftC (suc c) c (suc c) (Setoids c c))
  ; terminal = {!!}
  ; true = {!!}
  ; universal = λ {U} {X} {f} f-mono → record
    { _⟨$⟩_ = λ x → lift record
      { Carrier = {!!}
      ; _≈_ = {!!}
      ; isEquivalence = {!!}
      }
    ; cong = {!!}
    }
  ; pullback = {!!}
  ; unique = {!!}
  }

Because Ω now has isomorphisms inside of it, we can easily create the universal map of the pullback. The trouble comes in when we try to write out the universal map of the subobject classifier. Ideally, we would want something like:

 Σ[ u ∈ Setoid.Carrier U ] Setoid._≈_ X (f ⟨$⟩ u) x

However, this has type Set (suc c), and we need a Set c! More generally, no matter what we do, we can't quantify over U without going up a universe level, so we get stuck.

Taking a step back, this sort of makes sense. Agda is pretty predicative, and topoi are not, so no matter what we do we are going to run into trouble. We might want to look into ΠW-pretopoi, specifically the Predicative Topos of Bishop Sets.

[JacquesCarette]

There is nothing left to do here, so closing. But because this was such useful information, I have used the wiki to remember this