define _⇒_

UniMath · Dec 12, 2023 · d5f1565 · d5f1565
1 parent 676bf18
commit d5f1565
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md
@@ -178,7 +178,7 @@ Below, we outline a list of general rules when assigning associativities.
 | 15               | Parametric multiplicative operators like `_×_`,`_×∗_`, `_∧_`, `_∧∗_`, function composition operators like `_∘_`,`_∘∗_`, `_∘e_`, and `_∘iff_`, concatenation operators like `_∙_` and `_∙h_` |
 | 10               | Parametric additive operators like `_+_`, `_∨_`, `_∨∗_`, list concatenation, monadic bind operators for the type checking monad                                                             |
 | 6                | Parametric relational operators like `_＝_`, `_~_`, `_≃_`, and `_↔_`, elementhood relations, subtype relations                                                                              |
-| 5                | Directed function type-like formation operators, e.g. `_→∗_` and `_↪_`                                                                                                                      |
+| 5                | Directed function type-like formation operators, e.g. `_⇒_`, `_→∗_`, `_↠_`, `_↪_`, `_↪ᵈ_`, and `_⊆_`                                                                                        |
 | 3                | The pairing operators `_,_` and `_,ω_`                                                                                                                                                      |
 | 0-1              | Reasoning syntaxes                                                                                                                                                                          |
 | -∞               | Function type formation `_→_`                                                                                                                                                               |
diff --git a/src/foundation-core/propositions.lagda.md b/src/foundation-core/propositions.lagda.md
@@ -315,6 +315,9 @@ implication-Prop P Q = hom-Prop P Q
 type-implication-Prop :
   {l1 l2 : Level} → Prop l1 → Prop l2 → UU (l1 ⊔ l2)
 type-implication-Prop P Q = type-hom-Prop P Q
+
+infixr 5 _⇒_
+_⇒_ = implication-Prop
 ```
 
 ### The type of equivalences between two propositions is a proposition