Loop anima as a group object

Construction 2.4.24 (Loop anima as a group object). Given a pointed anima \(X \in \An _*\), we may consider the maps \begin {align*} e\colon * &\xrightarrow {(\id ,\id )} * \times _X * = \Omega X, \\ M \colon \Omega X \times \Omega X \cong * \times _X * \times _X * &\xrightarrow {(\pr _1,\pr _3)} * \times _X * = \Omega X, \hspace {20pt}\\ i\colon \Omega X = * \times _X * &\xrightarrow {(\pr _2,\pr _1)} * \times _X * = \Omega X. \end {align*}

These maps satisfy the usual group relations up to homotopy, so that \(\Omega X\) acquires the structure of a group object in \(\Ho (\An _*)\). We leave the details to the reader.