Removed notation for predicate operations.

UniMath · Dec 23, 2024 · bbe39a1 · bbe39a1
1 parent ec1d513
commit bbe39a1
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/code/Inductive/Predicates.v b/code/Inductive/Predicates.v
@@ -11,16 +11,10 @@ properties.
 Section Operations.
 
   Definition predconj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∧ (q x)).
-
-  Infix "p ∧ q" := (predconj p q) (at level 25).
 
   Definition preddisj {X : UU} (p q : X → hProp) : X → hProp := (λ x : X, (p x) ∨ (q x)).
 
-  Infix "p ∨ q" := (preddisj p q) (at level 25).
-
   Definition predneg {X : UU} (p : X → hProp) : X → hProp := (λ x : X, hneg (p x)).
-
-  Notation "¬ p" := (predneg p) (at level 35).
 
   Definition preddirprod {X Y : UU} (p : X → hProp) (q : Y → hProp) : (X × Y) → hProp := (λ x : X × Y, (p (pr1 x)) ∧ (q (pr2 x))). 
 
@@ -36,4 +30,6 @@ Section Operations.
 
   Definition truepred (X : UU) : X → hProp := (λ _ , htrue). 
 
+  Definition falsepred (X : UU) : X → hProp := (λ _, hfalse).
+
 End Operations.