#let Tm = $upright(bold("Tm"))$
#let Ty = $upright(bold("Ty"))$
#let Eq = $upright(bold("Eq"))$
#let Id = $upright(bold("Id"))$
#let Void = $upright(bold("Void"))$
#let absurd = $upright("absurd")$
#let Bool = $upright(bold("Bool"))$
#let tt = $upright("true")$
#let ff = $upright("false")$
#let inl = $upright("inl")$
#let inr = $upright("inr")$
#let zero = $upright("zero")$
#let succ = $upright("succ")$
#let hy= $tack.r$
#let type = $upright("type")$
#let sq = $upright(bold("q"))$
#let sp = $upright(bold("p"))$
#let Unit = $upright("Unit")$
#let El = $upright(bold("El"))$
#let code = $upright(bold("code"))$
#let UU = $upright(bold("U"))$
#let HProp = $upright(bold("HProp"))$
#let rec = $upright("rec")$
#let ind = $upright("ind")$
#let lift = $upright(bold("lift"))$
#let uni = $upright(bold("uni"))$
#let sym = $upright("sym")$
#let trans = $upright("trans")$
#let cong = $upright("cong")$
#let subst = $upright("subst")$
#let jrule = $upright(bold("J"))$
#let uniq = $upright("uniq")$
#let gap = $#h(0.3em)$
#let refl = $upright("refl")$
#let equiv = $tilde.eq$
#let idtoequiv = $upright("idtoequiv")$
#let isotoid = $upright("isotoid")$
#let ua = $upright("ua")$