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.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:su-207780 |
| Date | January 2022 |
| Creators | Åkerman Rydbeck, Carl |
| Publisher | Stockholms universitet, Matematiska institutionen |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0025 seconds