Please read the post more carefully. I’ve explained in the original post what this means and gave examples of the number pi being an inhabitant of the type of irrational numbers.
PS I’ll ask again that this thread remain on-topic about using formal languages (type theory, mathematics, logic) to clarify disagreements over doctrine. It has nothing to do with the tetralemma per se. I’m writing up a new thread for that topic as expressed in type-theoretic language, but even that one won’t be about generic debates around a point of doctrine without using formal languages.