(* -*- mode: coq; mode: visual-line -*- *)Require Import Truncations. Require Import Algebra.ooGroup. Require Import Spaces.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, _] _.