Convert a Variables to two Admitted statements in a Birmingham 2017 e…

…xercise set
UniMath · Sep 6, 2024 · 363cd9c · 363cd9c
1 parent 56a8a9d
commit 363cd9c
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v b/2017-12-Birmingham/Part5_Set_Level_Mathematics/set_level_mathematics_exercises.v
@@ -214,7 +214,11 @@ Definition isrefl {X : UU} (R : hrel X) : UU
 (* FILL IN THE DEFINITIONS OF istrans AND issymm *)
 (* Definition istrans {X : UU} (R : hrel X) : UU := *)
 (* Definition issymm {X : UU} (R : hrel X) : UU := *)
-Variables istrans issymm: forall {X: UU}, hrel X -> UU. (* to be deleted *)
+
+Definition istrans {X : UU} (R : hrel X) : UU.
+Admitted.
+Definition issymm {X : UU} (R : hrel X) : UU.
+Admitted.
 
 Definition ispreorder {X : UU} (R : hrel X) : UU := istrans R × isrefl R.