an involution is an equivalence

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

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
 ```
 
 <!--