TT^obs

The strict-proposition and proof-irrelevance headlines are

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢{\mathsf{SProp}}_i:{\mathcal{U}}_j$

$\mathrm{\Gamma }⊢P:{\mathsf{SProp}}_i$$\mathrm{\Gamma }⊢p:P$$\mathrm{\Gamma }⊢q:P$

$\mathrm{\Gamma }⊢p\equiv q:P$

Observational equality has formation and reflexivity

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_i$$\mathrm{\Gamma }⊢a:A$$\mathrm{\Gamma }⊢b:A$

$\mathrm{\Gamma }⊢a{\approx }_{A}b:{\mathsf{SProp}}_i$

$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢\mathsf{refl}:a{\approx }_{A}a$

and computes according to the full table of definition 79.11; $\mathsf{cast}$ has the rules of definition 79.17.