We define Integers in Homotopy Type Theory as a Higher Inductive Type (see Altenkirch and Scoccola - LiCS 2020). The purpose of program is to formalize the definition in the proof assistant cubical Agda and compare it with the traditional, normal-form and initial ring definitions of Integers. In the end we will formalize the proof that Integers form a commutative ring as well as other basic properties of Integers.
zoltan-balazs / hit-integers Goto Github PK
View Code? Open in Web Editor NEWFormalization of HIT Integers forming a commutative ring