It may be a bit early for me to ask this question, perhaps. I haven't used Lean beyond The Natural Numbers Game (Which was a lot of fun).
I'm reading Theorem Proving in Lean 4. It says stuff like:
Prop has some special features
and
if p : Prop is any proposition, Lean's kernel treats any two elements t1 t2 : p as being definitionally equal, [...]. This is known as proof irrelevance.
Does Prop get any special treatment in core? If not, how is proof irrelevance created? Is it just "naturally" a property of the bottom of the hierarchy of universes?
The related thing I've stumbled across is Propositional extensionality which has the following axiom:
axiom propext {a b : Prop} : (a ↔ b) → a = b
Is this the axiom that sort of creates proof irrelevance? Could I create a proof irrelevant analog to Prop with all the same properties/behaviors and start proving the same theorems again? (Not that I'd want to! of'c)
Prop has special treatment in the kernel. Any two proofs of a proposition are definitionally equal, and I guess this is just a built in feature, it's not "naturally" created.
propext is an axioms about equality of propositions. It doesn't create proof irrelevance. Note that propext deals with equalities of Props and proof irrelevance deals with equalities of proofs.
Something close to a proof irrelevant analog to Prop you could make is the type of Types with at most one element. So you could define Prop2 := { T : Type // ∀ x y : T, x = y }. However, this would not satisfy proof irrelevance by definition, the equalities would be propositional equalities and not definitional equalities.