%
\label{def:enrichment-frontier}
The \textbf{enrichment frontier classification}
assigns a novelty status to each transition
of the enrichment ladder:
\begin{enumerate}
    \item \textbf{$E_0 \to E_1$: Achieved.}
          Internalizing types within a categorical framework
          has been accomplished by multiple groups
          (Altenkirch--Kaposi \cite{AltenkirchKaposi2016},
          Bocquet--Kaposi--Sattler \cite{BocquetKaposiSattler2023},
          Moerdijk--Palmgren \cite{MoerdijkPalmgren2002}).
          Adaptation to $\tau$'s finite constructive
          non-Boolean setting is required but is not
          a theoretical barrier.
    \item \textbf{$E_1 \to E_2$: Partially achieved.}
          Internal proof-theoretic reasoning exists
          (Joyal arithmetic universes
          \cite{vanDijkGietelinkOldenziel2020}).
          Resource-sensitive type theory exists
          (graded modal DTT \cite{Abel2023},
          substructural DTT \cite{SubstructuralDTT2024}).
          The combination into a complete system
          internalizing full linear proof theory
          within a categorical framework
          has not been accomplished.
          Novel assembly of known tools.
    \item \textbf{$E_2 \to E_3$: Unprecedented.}
          No formal system of meaningful mathematical strength
          achieves full self-hosting.
          Willard \cite{Willard2001}: self-verification
          at sub-PA strength.
          Girard \cite{Girard2016TS,Eng2023}:
          fragments of linear logic from sub-logical operations.
          Williams--Stay \cite{WilliamsStay2021}:
          native $*$-autonomous type theory (programmatic).
          An open research problem.
\end{enumerate}