nLab Initiality Project - Type Theory - Term equality

$$\frac{ }{\Gamma \vdash T \equiv T : A}$$

$$\,$$

$$\frac{\Gamma \vdash T \equiv S : A}{\Gamma \vdash S \equiv T : A}$$

$$\,$$

$$\frac{\Gamma \vdash S \Leftarrow A \qquad \Gamma \vdash T \equiv S : A\qquad \Gamma \vdash S \equiv R : A}{\Gamma \vdash T \equiv R : A}$$

$$\,$$

$$\frac{\Gamma \vdash A\,type \qquad \Gamma \vdash T \equiv S : A \qquad \Gamma \vdash A \equiv B type}{\Gamma \vdash T \equiv S : B}$$