Is this axiom ok?

Stream: general

[deepest recursion]

Hello. I was wondering if this definition could be misused

axiom interchange_subtype {T:Type _}{P:T->Prop}(p₁:{v₁ // P v₁})(v₂:T)(p:P v₂): p₁ = ⟨ v₂ , p ⟩

To me it doesn't immediately appear as something that could cause trouble. Do you see any problems with it?

[Floris van Doorn]

This is inconsistent:

axiom interchange_subtype {T:Type _}{P:T->Prop}(p₁:{v₁ // P v₁})(v₂:T)(p:P v₂): p₁ = ⟨ v₂ , p ⟩

example : False := by
  have := interchange_subtype (P := fun _ : Bool ↦ True) ⟨true, trivial⟩ false trivial
  contradiction

[Edward van de Meent]

what this axiom says is: For any condition on a type, if the condition holds for p1 and p2, they are the same element.

[Edward van de Meent]

the example Floris gives takes advantage of the fact that there are multiple elements of Bool (that satisfy the trivial (always true) condition), which results in (according to your axiom) true=false, which of course is a contradiction.

[Edward van de Meent]

i imagine that this isn't quite the axiom you wanted to introduce...

[Edward van de Meent]

could you describe it?