I have a question regarding propositional truncation $||$-$||$ in homotopy type theory. According to the introduction rule of $||$-$||$, if $a:A$, then $|a|:||A||$. My question is, if $||A||$ is inhabited, what about $A$? Does it imply that $A$ is inhabited (though the inhabitant is unknown/underspecified)?
If we think $|$-$|:A\rightarrow||A||$ as a way to hide information (i.e., proof objects of $A$), then that means that such information must exist, right? Though it's in an anonymous/underspecified way...
I am not sure if my understanding is correct. Let me know if I get it wrong.
I think that your understanding is correct.
The only way to build an inhabitant of $\|A\|$ is to use an inhabitant of $A$. So you can say that "intuitively" if $\|A\|$ is inhabited then $A$ is inhabited, but that does not mean that you have a map $f:\|A\|\rightarrow A$.
Propositional truncation hides information, but sometimes in a surprising way, as shown by N. Kraus here, and further discussed here.