range coe for sets

Stream: general

[Oliver Nash]

This might be a dumb question but I just bumped into the fact that subtype.range_coe is not true by rfl. More precisely:

import data.set.basic

open set

example {α : Type*} (s : set α) : range (coe : s → α) = s := subtype.range_coe -- But not true by `rfl`

example {α : Type*} (s : set α) : range (coe : s → α) = s :=
begin
  -- This is what we trying to prove; it's obviously not true by definition
  change (λ (x : α), ∃ (y : ↥s), coe y = x) = s,
  ext z,
  -- Even granting extensionality, it's obviously still not true by definition
  change (∃ (y : ↥s), coe y = z) ↔ z ∈ s,
  -- etc.
  sorry,
end

[Oliver Nash]

Of course this doesn't really matter but I wondered if things had to be this way. Could we have a library of sets where we had this by definition?

[Johan Commelin]

I think it will be really hard to make that defeq. But I don't know how to make my intuition precise.

[Oliver Nash]

That was basically my conclusion also. There might not be much more to say here.

[Mario Carneiro]

I agree with Johan. One way to make it a bit more clear is to consider what happens if we treat it as a computable function, under the substitution Prop |-> Type. In that case, we are composing coe s : (Σ x: A, s x) -> A with range : (A -> B) -> B -> Type and wish for range (coe s) x = s x to be defeq. The definition of coe here is basically set in stone (it is the first projection), so the only question is whether there is a definition of range making this work. Like this:

namespace test

def coe {A : Type} (s : A → Type) : (Σ x, s x) → A := λ p, p.1

def range {A B : Type} : (A → B) → B → Type :=
sorry -- λ f b, Σ a, plift (f a = b)

example {A} (s : A → Type) (x : A) : range (coe s) x = s x := rfl -- ??

end test

Notice that this is an equality of types. Since there are no reductions or cancellations at the level of type operators, the only way we could hope to have range (coe s) compute to s would be if it was (directly or indirectly) an input to range, but the implicit arguments are @range (Sigma s) A (coe s), so we are stymied by the fact that Sigma is not an injective type operator (certainly not at the defeq level).

[Oliver Nash]

Thanks Mario, this is the sort of great answer I had hoped I might receive if I was lucky!