Two-Level Type Theory and Strict Equality

Opening obstruction

Coherence, internal syntax, and staging sometimes require strict equations, but reflecting all fibrant identity would collapse homotopical structure and conversion.

Development contract

Use the Annenkov–Capriotti–Kraus–Sattler two-level signature: the outer judgment has reflected strict equality with UIP, the inner judgment has fibrant identity, and conversion from inner to outer types supplies no reflection rule back into fibrant identity. Prove the presheaf-model conservativity theorem and calculate the first three semisimplicial levels using strict boundary equations; axiomatic univalence remains noncomputing.