IdemInvo.idr

module IdemInvo

%default total

-- The properties

Idem : (a -> a) -> Type
Idem f = (x : _) -> f (f x) = f x

Invo : (a -> a) -> Type
Invo f = (x : _) -> f (f x) = x

-- Examples:

Id : a -> a
Id = id

idIsIdem : Idem Id
idIsIdem _ = Refl

Const : a -> b -> a
Const = const

constIsIdem : (x : a) -> Idem (Const x)
constIsIdem _ _ = Refl

Flip : Bool -> Bool
Flip = not

notIsInvo : Invo Flip
notIsInvo False = Refl
notIsInvo True = Refl

Xor : Bool -> Bool -> Bool
Xor False False = True
Xor False True = False
Xor True False = False
Xor True True = True

xorIsInvo : (x : Bool) -> Invo (Xor x)
xorIsInvo False False = Refl
xorIsInvo False True = Refl
xorIsInvo True True = Refl
xorIsInvo True False = Refl

-- If both, must be id!

idemInvoIsId : (f : a -> a) -> Idem f -> Invo f -> (x : a) -> f x = id x
idemInvoIsId f idem invo x =
  rewrite sym (idem x) in
  rewrite sym (invo x) in
  Refl