# 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

**Abstract:**

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.