@article {10.3844/jmssp.2022.148.162,
article_type = {journal},
title = {Formalizing Relations in Type Theory},
author = {Kachapova, Farida},
volume = {18},
year = {2022},
month = {Oct},
pages = {148-162},
doi = {10.3844/jmssp.2022.148.162},
url = {https://thescipub.com/abstract/jmssp.2022.148.162},
abstract = {Typetheory plays an important role in the foundations of mathematics as a frameworkfor formalizing mathematics and a base for proof assistants providingsemi-automatic proof checking and construction. Derivation of each theorem intype theory results in a formal term encapsulating the whole proof process.This study uses a variant of type theory, namely the Calculus of Constructionswith Definitions, to formalize the standardtheory of binary relations. This includes basic operations on relations,criteria for special properties of relations, invariance of these propertiesunder the basic operations, equivalence relation, well-ordering, andtransfinite induction. Definitions and proofs are presented as flag-stylederivations.},
journal = {Journal of Mathematics and Statistics},
publisher = {Science Publications}
}