Definitional equality in a Prop?

Stream: general

[Arnoud van der Leer]

I have been trying to port some code about presheafed spaces from mathlib4 to UniMath (a univalent foundations library, written in coq). However, I had a bit of trouble doing that. There even are some proof statements that do not typecheck when ported to UniMath. When searching for the root cause for this, I started suspecting that elements of a Prop are definitionally equal. For example, in Lean this seems to work:

theorem map_along_id
  (U : (Opens β))
  : U = (comap (ContinuousMap.id β)) U := by
    rfl

Whereas in UniMath / coq its equivalent would give a "cannot unify U with (comap (ContinuousMap.id β)) U" error.

Is this indeed true? Are all elements of a Prop definitionally equal in Lean? I.e., if we have some type $T = \sum_{x : X} P x$ with $P : Prop$, and we have a dependent type $A: T \to Type$, is it then true that if we have $x: X$ and $p, q: P x$ and $a: A (x, p)$, we also have $a: A(x, q)$? Does this not lead to problems?

[Sébastien Gouëzel]

Yes, it's true in Lean's type theory. It's called proof irrelevance. No, it doesn't create problems.

[Sébastien Gouëzel]

See SProp in Coq/Rocq.

[Arnoud van der Leer]

Ah, thanks :-)
I always thought proof irrelevance was an axiom, but in Lean, it is builtin.

[Arnoud van der Leer]

And thanks, I'll take a look at SProp