Internalizing judgemental structure

A well-justified connective (i.e. way of introducing types and their terms) abides the following:

Slogan 2.5.4

A connective in type theory is given by (1) a natural type-forming operation $Υ$ and (2) one of the following:

a natural isomorphism relating $T m (Γ, Υ)$ to judgementally-determined structure, or
a collection of natural term constructors for $Υ$ which, for all dependent types $Γ . Υ ⊢ 𝐴$ , determine a natural isomorphism relating $T m (Γ . Υ, 𝐴)$ to judgementally-determined structure.¹

The first camp accounts for the most well-behaved connectives, the latter for inductive types.

See also