From d5f15650556cd52ebac0f577592e34b940ec2779 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 12 Dec 2023 18:05:46 +0100 Subject: [PATCH] =?UTF-8?q?define=20`=5F=E2=87=92=5F`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- MIXFIX-OPERATORS.md | 2 +- src/foundation-core/propositions.lagda.md | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/MIXFIX-OPERATORS.md b/MIXFIX-OPERATORS.md index aa6021c8ef..062281d9f7 100644 --- 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 index a7f898320f..dac8e67302 100644 --- 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