The free group in Cubical Agda

FreeGroup.agda

{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude

infix  1 begin_
begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

infix  9 _⁻¹
infixl 5 _·_

data Group : Set where
  e : Group
  _·_ : Group → Group → Group
  _⁻¹ : Group → Group
  assoc : (x y z : Group) → (x · y) · z ≡ x · (y · z)
  idˡ : (x : Group) → e · x ≡ x
  idʳ : (x : Group) → x · e ≡ x
  invˡ : (x : Group) → x ⁻¹ · x ≡ e
  invʳ : (x : Group) → x · x ⁻¹ ≡ e

unique-idˡ : (e' : Group) → ((x : Group) → e' · x ≡ x) → e' ≡ e
unique-idˡ e' h = sym (idʳ e') ∙ h e

unique-idʳ : (e' : Group) → ((x : Group) → x · e' ≡ x) → e' ≡ e
unique-idʳ e' h = sym (idˡ e') ∙ h e

unique-inv : {x x' : Group} → x · x' ≡ e → x' ≡ x ⁻¹
unique-inv {x} {x'} h =
  begin
    x'
  ≡⟨ sym (idˡ x') ⟩
    e · x'
  ≡⟨ cong (_· x') (sym (invˡ x)) ⟩
    (x ⁻¹ · x) · x'
  ≡⟨ assoc (x ⁻¹) x x' ⟩
    x ⁻¹ · (x · x')
  ≡⟨ cong (x ⁻¹ ·_) h ⟩
    x ⁻¹ · e
  ≡⟨ idʳ (x ⁻¹) ⟩
    x ⁻¹
  ∎

inv-id : e ⁻¹ ≡ e
inv-id =
  begin
    e ⁻¹
  ≡⟨ sym (idˡ (e ⁻¹)) ⟩
    e · e ⁻¹
  ≡⟨ invʳ e ⟩
    e
  ∎

inv-mul : {x y : Group} → (x · y) ⁻¹ ≡ y ⁻¹ · x ⁻¹
inv-mul {x} {y} =
  sym (
    unique-inv
      (begin
        (x · y) · (y ⁻¹ · x ⁻¹)
      ≡⟨ assoc x y (y ⁻¹ · x ⁻¹) ⟩
        x · (y · (y ⁻¹ · x ⁻¹))
      ≡⟨ cong (x ·_) (sym (assoc y (y ⁻¹) (x ⁻¹))) ⟩
        x · ((y · y ⁻¹) · x ⁻¹)
      ≡⟨ cong (λ g → x · (g · x ⁻¹)) (invʳ y) ⟩
        x · (e · x ⁻¹)
      ≡⟨ cong (x ·_) (idˡ (x ⁻¹)) ⟩
        x · x ⁻¹
      ≡⟨ invʳ x ⟩
        e
      ∎)
  )

inv-inv : {x : Group} → (x ⁻¹) ⁻¹ ≡ x
inv-inv {x} = sym (unique-inv (invˡ x))