This record contains a unified presentation of two related papers: (1) Stratified Negation and a 2-Categorical Non-Embedding Theorem,(2) Coherence Growth in Homotopy Type Theory via Monad Dynamics. The two works are unified by a common higher-categorical perspective in which:- coherence phenomena arise from iterated identity structures in homotopy type theory,- while negation is modeled as a generative colimit-based operation in a weak 2-categorical setting. The coherence theory is formulated internally in an (∞,1)-topos in the sense of Lurie, where iterated identity types induce a monadic or iterative refinement structure. In contrast, the negation theory is developed in a weak 2-categorical framework using spans and pushout constructions that generate non-confluent behavior. The main conceptual point of the combined framework is that coherence-preserving structures and generative negation structures cannot, in general, be simultaneously strictified into a 1-categorical or algebraically closed setting. This incompatibility is formulated as a structural non-embedding phenomenon. While the coherence side includes a dynamical interpretation via homotopy cardinality and asymptotic growth (partly conjectural), the negation side focuses on categorical construction principles and structural obstructions. The two theories are presented as complementary aspects of a stratified higher-categorical system rather than as independent frameworks.
Yugo Hidaka (Sat,) studied this question.