Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
From HoTT Require Import Basics.From HoTT Require Import Basics.
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.