From 4988c414654eb26bdfda5e309d02ebb400930a90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Na=C3=AFm=20Favier?= <n@monade.li>
Date: Mon, 18 Dec 2023 12:43:20 +0100
Subject: [PATCH] an involution is an equivalence

---
 src/1Lab/Equiv.lagda.md | 7 +++++++
 src/Data/Bool.lagda.md  | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index 4aaffcfe3..4a73f9cb9 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -607,6 +607,13 @@ is-empty→≃⊥ : ∀ {ℓ} {A : Type ℓ} → ¬ A → A ≃ ⊥
 is-empty→≃⊥ ¬a = _ , ¬-is-equiv ¬a
 ```
 
+Any involution is an equivalence:
+
+```agda
+is-involutive→is-equiv : ∀ {ℓ} {A : Type ℓ} {f : A → A} → (∀ a → f (f a) ≡ a) → is-equiv f
+is-involutive→is-equiv inv = is-iso→is-equiv (iso _ inv inv)
+```
+
 # Equivalence reasoning
 
 To make composing equivalences more intuitive, we implement operators to
diff --git a/src/Data/Bool.lagda.md b/src/Data/Bool.lagda.md
index d553bfd0a..a3a8c9cb3 100644
--- a/src/Data/Bool.lagda.md
+++ b/src/Data/Bool.lagda.md
@@ -321,7 +321,7 @@ equivalence:
 
 ```agda
 not-is-equiv : is-equiv not
-not-is-equiv = is-iso→is-equiv (iso not not-involutive not-involutive)
+not-is-equiv = is-involutive→is-equiv not-involutive
 ```
 
 <!--