3.4 "Propositions are types, so true is a type, but one that inhabits Prop; and it has one constant constructor and that’s the one and only proof, intro.That’s it!" --> Are you saying that the proposition can be assigned to its one and only proof? But aren't they technically different types? Or are both Props (or maybe both are in the overarching class of Type?) But both being in the same class would not make sense as it's a hierarchy of universes with different types as I understand it!

[RoboticMind]

Here's how I would clarify it:

true.intro is of type true but true is of type Prop

#check true.intro
true.intro : true

#check true
true : Prop

A proof of a proposition has the type of that specific proposition. So true.intro is of type true using and introduction rules with X and Y would give a term of type X ∧ Y. Neither term, however is of type Prop but yes the type of true or X ∧ Y is Prop

It's also worth mentioning that propositions may have multiple proofs. Or they might not have any proofs at all in the case of false or 0=1 so there are no terms of type false or 0=1