(* -*- mode: coq; mode: visual-line -*-  *)

Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.ooGroup.

Local Open Scope path_scope.

(** * Actions of oo-Groups *)

Definition ooAction (G : ooGroup)
  := classifying_space G -> Type.

Definition action_space {G} : ooAction G -> Type
  := fun X => X (point _).

Coercion action_space : ooAction >-> Sortclass.