Type Theory enables mathematicians to perform proofs in a formal language that
computers can understand. This enables computer-assisted proofs and the computerization of all mathematical knowledge. Homotopy Type Theory (HoTT) views types as topological spaces, unlocking new ways to understand and expand Type Theory. One of the most interesting expansions of Type Theory thanks to HoTT has been the development of the Univalence Axiom which expands the definition of "equality between types". This paper analyses the work done in the paper "Isomorphims is Equality"and applies their proof of Univalence for higher structures to two specific monoids on sets. This is done in terminology that is understandable to Computer Scientists with the aim to further the collaboration between the two fields.