Having witnessed a debate between a categorical logician/type-theorist and a model theorist, I think there is still (sometimes heated) disagreement about how well different mathematical formalisms “reflect the actual nature of math” amongst people who know these theories at the expert level.
I’ll provide a simple answer while we await a more informed one. I think a good type theorist told me that type theory is just logic with a conceptual extension where propositions need “witnesses”. In logic, if you take a collection of formulas and use a deductive calculus such as sequent calculus to derive theorems, your ability to arrive at a particular formula by applications of those deductive rules constitutes a “proof”. Writing a proof amounts to saying, “if those axioms are true, then this formula is true”. You don’t write “is true” next to a formula, but you just show how the formula can be arrived at from other formulas.
In type theory, a distinction is made between (I think) propositions and judgments! I think this is a distinguishing feature of type theory, and it was identified by Per Martin-Löf. I think the difference is that in type theory, there is an explicit syntax for distinguishing between a proposition merely as a unit of meaning, vs. judging “and this proposition is true (or false)”.
I think you prove a proposition is true by proving that the proposition has a “witness”, which is the type-theoretic way of judging “this proposition is true”. It is written p : P. I think p is the term, and P is the type. I think if P is of type “Proposition”, then proving the type is what is called inhabited (i.e., we know there exists at least one term of that type) means we have found a witness, i.e., proved or judged it true.
I think the answer to your question requires a technical understanding of type theory. But to answer your question of if types are propositions or are just represented as propositions, I think the former. In a blog post by Astra Kolomatskaia and Mike Shulman, they discuss how one way type theory and set theory are paradigmatically different (at least how I understood it) is that type theory in some ways is more “conceptually faithful” than set theory. Set theory is like an encoding of information and structures, but type theory allows you to define a better depiction of the logical world by allowing you to designate different categories of things from the beginning.
The introduction to the book “Categorical Logic and Type Theory” corroborates this:
This is probably a very good resource to read further on this:
In type theory, the paradigm of propositions as types says that
propositions and types are essentially the same. A proposition is
identified with the type (collection) of all its proofs, and a type is
identified with the proposition that it has a term (so that each of
its terms is in turn a proof of the corresponding proposition).
… to show that a proposition is true in type theory corresponds to
exhibiting an element “term” of the type corresponding to that
proposition. We regard the elements of this type as evidence or
witnesses that the proposition is true. (They are sometimes even
called proofs… (from Homotopy Type Theory – Univalent Foundations of
Mathematics, section 1.11)
…Accordingly, logical operations on propositions have immediate
analogs on types. For instance logical ‘and’ corresponds to forming
the product type A×B(a proof of A and a proof of B), the universal
quantifier corresponds to dependent product, the existential
quantifier to dependent sum. In classical mathematics, the law of
double negation corresponds to a global choice operator.
