Question

I would like to clarify the precise difference between the phrases "statement inside/ internal the theory" and "statement about the theory" in context of Homotopy Type Theory.

A naive guess: can an 'internal statement' be understood as an abstract 'type' and the the decision about if the statement is true or not depends on if this type is 'inhabited' by some object (which would - if it exists-tautotologically have this type).

And in contrast, a "statement about the theory" shall be an inference rule, not more not less?

Is this interpretation correct or does it missing the point?

ADDENDUM: When I initially posed this question I forgot to add/ mention that probably the concept of a judgment should better reflect what might be regarded as an "external statement/ statement about the theory". So finally the partial question is: is "judgment" what should be recognized as synonymous term for "external statement"?

Answer 1

A 'statement inside the theory' in Homotopy Type Theory relates to a statement expressible within the theory's framework, often tied to the existence of an object that inhabits a type. A 'statement about the theory' conversely discusses the theory itself, possibly from a meta-theoretical standpoint, including its rule systems and its broader properties. 'Judgment' in type theories align with statements about the theory, indicating formal assertions regarding the theory's foundational constructs.

Step-by-step explanation:

In the context of Homotopy Type Theory, the distinction between 'statement inside the theory' and 'statement about the theory' revolves around where the statement resides in relation to the theoretical framework. A 'statement inside the theory' typically refers to a statement that can be expressed using the constructs of the theory itself, akin to saying that something 'holds' within the theoretical world we are considering. This indeed depends on whether the type in question is inhabited by some object. For example, in the language of types, a type is true if it is inhabited, which aligns with your interpretation.

On the other hand, a 'statement about the theory' relates to a meta-level discussion regarding the theory, such as the inference rules that govern it or properties of the theory as a whole. This could encompass statements or judgments that evaluate or analyze the theory from an external viewpoint.

You also brought up the term 'judgment', which in the context of type theory, does correspond more closely with an external statement or a statement about the theory. A judgment is a formal assertion about types and terms within a type theory and may pertain to things like the validity of a type or the assignment of a term to a type, which are foundational aspects with regards to how we understand and interpret the theory externally.