agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

454 stars 139 forks source link

Typevariate and list-based polynomials are isomorphic #922

Closed felixwellen closed 2 years ago

felixwellen commented 2 years ago

This PR shows that there is an isomorphism of algebras between the typevariate polynomials (with index type Unit) defined as a HIT and the list-based polynomials. Depends on #917

felixwellen commented 2 years ago

917 merged -> ready for review.

felixwellen commented 2 years ago

...once the conflicts are resolved.