Formalizing {$\\Pi$}4({{S3}}) {$\\cong$}{{Z}}/{{2Z}} and {{Computing}} a {{Brunerie Number}} in {{Cubical Agda}}