Review of 'I-words'

This section of the book is primarily a review of material covered in previous Articles and Sessions, but it includes one new definition.

Definition: Involution (p. 118)

If {f \circ f = 1_A}, we say f is an involution.

We implement Involution and IsInvolution in Lean as follows:

structure Involution {𝒞 : Type u} [Category.{v, u} 𝒞] (A : 𝒞) where
  f : A ⟶ A
  invol : f ⊚ f = 𝟙 A

class IsInvolution {𝒞 : Type u} [Category.{v, u} 𝒞] {A : 𝒞}
    (f : A ⟶ A) where
  invol : f ⊚ f = 𝟙 A