{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Functions.Involution where

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

isInvolution : ∀{} {A : Type }  (A  A)  Type _
isInvolution f =  x  f (f x)  x

module _ {} {A : Type } {f : A  A} (invol : isInvolution f) where
  open Iso

  involIso : Iso A A
  involIso .fun = f
  involIso .inv = f
  involIso .rightInv = invol
  involIso .leftInv = invol

  involIsEquiv : isEquiv f
  involIsEquiv = isoToIsEquiv involIso

  involEquiv : A  A
  involEquiv = f , involIsEquiv

  involPath : A  A
  involPath = ua involEquiv

  involEquivComp : compEquiv involEquiv involEquiv  idEquiv A
  involEquivComp
    = equivEq  i x  invol x i)

  involPathComp : involPath  involPath  refl
  involPathComp
    = sym (uaCompEquiv involEquiv involEquiv) ∙∙ cong ua involEquivComp ∙∙ uaIdEquiv

  involPath² : Square involPath refl refl involPath
  involPath²
    = subst  s  Square involPath s refl involPath)
        involPathComp (compPath-filler involPath involPath)