Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.
Require Import Algebra.ooGroup.
Require Import Universes.BAut.
Require Import Pointed.Core.

Local Open Scope pointed_scope.

(** * Automorphism oo-Groups *)

(** We define [Aut X] using the pointed, connected type [BAut X]. *)
Definition Aut (X : Type) : ooGroup
  := Build_ooGroup [BAut X, _] _.