This is a formalization in cubical Agda of division by two in type theory, as detailed in this article.
The main result here is that
A × 2 ≃ B × 2
implies
A ≃ B
where A and B are arbitrary types and 2 is a type with two elements
(e.g. the booleans).
The proof is based on the explanation of given in Doyle and Conway's Division by three, and you can nicely read the Agda code here.