Generalizable All Variables.

From Prelude Require Import Control Equality.

#[local]
Open Scope prelude_scope.

Definition identity_equal `{Equality a} (x y : id a) : Prop := x == y.

Instance id_Equality `{Equality a} : Equality (id a)|1000 :=
  { equal := identity_equal
  }.

Definition identity_map {a b} (f : a -> b) (x : id a) : id b :=
  f x.

#[program, universes(polymorphic)]
Instance identity_Functor : Functor id|1000 :=
  { map := @identity_map
  }.

Next Obligation.
  reflexivity.
Qed.

Next Obligation.
  reflexivity.
Defined.

Definition identity_apply {a b} (f : id (a -> b)) (x : id a) : id b :=
  f x.

Definition identity_pure {a} (x : a) : id a := x.

#[program]
Instance identity_Applicative : Applicative id|1000 :=
  { pure := @identity_pure
  ; apply := @identity_apply
  }.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Definition identity_bind {a b} (x : id a) (f : a -> id b) : id b :=
  f x.

#[program]
Instance identity_Monad : Monad id|1000 :=
  { bind := @identity_bind
  }.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.

Next Obligation.
  reflexivity.
Defined.