Wild groups

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-07.
Last modified on 2023-03-14.

module structured-types.wild-groups where
Imports 
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.wild-monoids

is-wild-group-Wild-Monoid :
  {l : Level} (M : Wild-Monoid l) → UU l
is-wild-group-Wild-Monoid M = is-binary-equiv (mul-Wild-Monoid M)

Wild-Group : (l : Level) → UU (lsuc l)
Wild-Group l = Σ (Wild-Monoid l) is-wild-group-Wild-Monoid

Recent changes