Why do Leans `Prop`ositions get special treatment?

Question

A question is nagging me since I began going through the interactive Lean tutorial: What is the purpose of the separate Prop hierarchy within Type?

As I understand it now, we have the following universe hierarchy in place:

Type (n+1)
  |   \
  |   Sort (n+1)
  |     |
Type n  | (?)
  |   \ |
 ...  Sort n
  |     |
Type 0 ... (?)
  |   \ |
 nat  Prop
  |     |
  0   p ∧ q
        |
     ⟨hp, hq⟩

1. Are the edges marked with ? actually there or did I just make them up (probably)?
2. From a swift look into Agda and Idris it seems they don't do the distinction between Sort n and Type n. Why does Lean distinguish them?

What feels weird about Prop is that it's like an inductive type on the one hand (e.g. the fact it's closed means p ∧ nat doesn't make sense) but used like a kind on the other hand (e.g. show type p : Prop to be inhabitated by constructing a proof value for p). I suspect that has something to do with the distinction, but I can't articulate it. Is there some basic paper to read this up?

Answer 1

There is just a single hierarchy of nat-indexed universes Sort u. From Chapter 3 of Theorem Proving in Lean:

In fact, the type Prop is syntactic sugar for Sort 0, the very bottom of the type hierarchy described in the last chapter. Moreover, Type u is also just syntactic sugar for Sort (u+1).

The idea of having an impredicative bottom universe Prop and a predicative hierarchy Type u on top of it was introduced in the Extended Calculus of Constructions. Lean introduces Sort as a single generalized hierarchy so that definitions can range over all universes using Sort u instead of needing separate definitions for Prop and for Type u.

In contrast, the bottom universe in Idris and Agda does not do anything special and thus they use a single name for their entire hierarchy.