Aren't the puzzles giving proofs of univalence of **Partitions**? Or perhaps something similar to it?