Skip to main content

Carl Åkerman Rydbeck: Formalisation of Polynomials in Cubical Type Theory Using Cubical Agda

Bachelor thesis presentation

Time: Thu 2022-06-09 10.00 - 11.00

Location: Kräftriket, house 6, room 306

Respondent: Carl Åkerman Rydbeck


We formalise polynomials over commutative rings in cubical type theory using Cubical Agda as proof assistant. On the basis of a formalisation of polynomials as number sequences with only a finite number of non-zero values, we use higher inductive types to formulate a list-based definition using two point constructors and two path constructors. The combinatorial explosion in proofs leads us to a redefinition: One of the path constructors is discarded, and instead we formulate a separate function-based definition. We prove equivalence of these distinct definitions, and use the function-based definition to provide a witness for the discarded path constructor. The list-based definition is then used in combination with this witness to prove that the resulting structure is itself a commutative ring.