Fix one problem that arose because of the displayed algebra change (#56)

Author: arnoudvanderleer

2024-07-Minneapolis/5_Set-level-mathematics/set_level_mathematics_solutions.v

@@ -282,7 +282,7 @@ Proof.
     + intros i. use proofirrelevance. use isapropismonoidop.
     + intros i. induction i. use idpath.
     + use setproperty.
-    + use isapropifcontr. exact (@isapropismonoidop X (pr2 X) Xop Yop).
+    + use isapropifcontr. exact (@isapropismonoidop (pr1setwithbinop X) (pr2 X) Xop Yop).
 Defined.
 Opaque monoid_univalence_weq2.