fact: Definition equiv_involution {X : Type} (f : X -> X) (isinvol : f o f == idmap) : X <~> X := equiv_adjointify f f isinvol isinvol.
imports: Basics.Overture Basics.PathGroupoids Basics.Contractible Basics.Tactics