Library Exercise_3_2_1_11


Require Import Utf8.
Require Import Common Monoid Group.
Import the ComputationalGroupOfAutomorphisms, and Isomorphism, for coercions.
Require Import Exercise_3_2_1_7 Isomorphism.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 3.2.1.11

Problem

Let X be a set and consider the group of permutations of X (see Exercise 3.2.1.7), which we will denote Σ X. Find a canonical action of Σ X on X.
  Let Σ := ComputationalGroupOfAutomorphisms.
  Variable X : Type.

  Definition ComputationalGroupOfAutomorphismsAction : MonoidAction (Σ X) X
    := {| monoid_action := ((λ f x, f x) : Σ X X X);
          is_monoid_action := (Build_IsMonoidAction (Σ X) (λ f x, f x)
                                                    (fun _ eq_refl)
                                                    (fun _ _ _ eq_refl)) |}.
End Exercise_3_2_1_11.