Merge pull request #54 from arnoudvanderleer/fix-variables

Convert a Variables to two Admitted statements
UniMath · Sep 10, 2024 · 752abd3 · 752abd3
2 parents 56a8a9d + 363cd9c
commit 752abd3
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.