In constructive type theories, we make a distinction between extensional and intensional identity types. It's trivial that extensional identity types are proof-irrelevant as the inhabitant of an extensional identity type is a constant $\textsf{eq}:\textsf{Eq}(a,b,A)$ (for $a,b:A$ and $a=b:A$). Regarding intensional identity types, I have two questions:
Let $A$ be an arbitrary type, is the intensional identity type $\textsf{Id}(a,b,A)$ (for $a,b:A$ and $a=b:A$) proof-irrelevant?
Let $A$ be a proof-irrelevant type, is $\textsf{Id}(a,b,A)$ (for $a,b:A$ and $a=b:A$) proof-irrelevant?
Note: A type $A$ is said to be proof-irrelevant iff $A$ satisfies: $(\Pi x,y:A)\textsf{Id}(x,y,A)$.
Thanks in advance!
This is not provable or disprovable in intensional type theory. You can add it as an axiom (uniqueness of identity proofs, UIP), or add axioms which imply its negation. Extensional type theory does the former, homotopy type theory the latter. The univalence axiom in HoTT implies the negation of UIP.
Yes. See Lemma 3.3.4 in the HoTT book, or Chapter 7 for a more general treatment.
In general, types have h-levels, which measures the amount of relevant information in identity types. Level $0$ has types which are equivalent to the unit type, and level $(n+1)$ has types whose identity types are at level n. In the book, levels start from $-2$ for historical reasons, but sometimes people start from $0$. If a type is at level $n$, it is also at level $(n + 1)$, hence its identity type is also at level $n$. Since being at level $1$ is the same as being proof-irrelevant, a proof-irrelevant type has proof-irrelevant identity types.
These results about h-levels hold in plain intensional type theory, with no HoTT-specific features required.