\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x_{1},x_{2}:C\)を対象、\(f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)を射とすると、型\(\mathord {\textnormal {\textsf {IsIso}}}(f)\)は命題である。
\(i\)を階数、\(C:\mathord {\textnormal {\textsf {PreCat}}}(i)\)を前圏、\(x_{1},x_{2}:C\)を対象、\(f:\mathord {\textnormal {\textsf {Map}}}(x_{1},x_{2})\)を射とすると、型\(\mathord {\textnormal {\textsf {IsIso}}}(f)\)は命題である。