I've been learning about free objects in category theory.Bartosz Milewski's Category Theory for Programmers has been particularly very informative.

An investigation into what assumptions which you can derive the ubiquitous lerp function and it's proprieties.

Playing with the Hom Functor to better understand it.

I'm hoping to prove Zeckendorf's theorem in Coq without reference as a personal challenge.

I'm trying to (mostly) faithfully translate a theorem from the Bird-Meertens Formalism Wikipedia article into Coq.