Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment