nLab Initiality Project - Type Theory - Type equality

ΓAAtype\frac{}{\Gamma \vdash A \equiv A type}
\,
ΓABtypeΓBAtype\frac{\Gamma \vdash A \equiv B type}{\Gamma \vdash B \equiv A type}
\,
ΓBtypeΓABtypeΓBCtypeΓACtype\frac{\Gamma \vdash B\,type\qquad \Gamma\vdash A \equiv B type \qquad \Gamma\vdash B \equiv C type}{\Gamma \vdash A \equiv C type}

Last revised on October 31, 2018 at 13:41:34. See the history of this page for a list of all contributions to it.