From 363cd9c4eca451e16f1f1d2d395fe8670fdb83f2 Mon Sep 17 00:00:00 2001 From: Tempestas Ludi Date: Fri, 6 Sep 2024 15:56:23 +0200 Subject: [PATCH] Convert a Variables to two Admitted statements in a Birmingham 2017 exercise set --- .../set_level_mathematics_exercises.v | 6 +++++- 1 file changed, 5 insertions(+), 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 index b7d4014..08e1b5d 100644 --- 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.