Are these “type erasure” axioms consistent?

Stream: Type theory

[Sabrina Jewson]

This is a bit of a random question, but are the following axioms consistent with Lean?

axiom Opaque.{u} : Type u
axiom to_opaque.{u} {α : Type u} : α → Opaque.{u}
axiom of_opaque.{u} {α : Type u} (o : Opaque.{u}) (h : ∃ a : α, to_opaque a = o) : α
axiom of_to_opaque.{u} {α : Type u} (a : α) : of_opaque (to_opaque a) ⟨a, rfl⟩ = a

And if so, what about if I remove the universe parameter on Opaque (presumably not, single that would allow smuggling large values in small places). Are there any papers related to this kind of concept?

[Kyle Miller]

If it were axiom Opaque.{u} : Type (u + 1) it seems like you could probably implement this with def Opaque.{u} : Type (u + 1) := Σ α : Type u, α, but with Type u I wouldn't be surprised if someone could cook up a paradox.

[Mario Carneiro]

import Mathlib.Logic.Function.Basic

axiom Opaque.{u} : Type u
axiom to_opaque.{u} {α : Type u} : α → Opaque.{u}
axiom of_opaque.{u} {α : Type u} (o : Opaque.{u}) (h : ∃ a : α, to_opaque a = o) : α
axiom of_to_opaque.{u} {α : Type u} (a : α) : of_opaque (to_opaque a) ⟨a, rfl⟩ = a

example : False :=
  Function.cantor_injective to_opaque.{0} fun a b h => by
    rw [← of_to_opaque a, ← of_to_opaque b]; congr

[Mario Carneiro]

and here's a proof of Kyle's claim that this can be done if you universe bump Opaque:

def Opaque.{u} : Type (u + 1) := Σ α : Type u, α
def to_opaque.{u} {α : Type u} : α → Opaque.{u} := fun a => ⟨_, a⟩
def of_opaque.{u} {α : Type u} (o : Opaque.{u}) (h : ∃ a : α, to_opaque a = o) : α :=
  let ⟨β, a⟩ := o
  cast (by rcases h with ⟨_, ⟨⟩⟩; rfl) a
theorem of_to_opaque.{u} {α : Type u} (a : α) : of_opaque (to_opaque a) ⟨a, rfl⟩ = a := rfl

[Sabrina Jewson]

Thank you! That makes a lot of sense.