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 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, _] _.