    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some derivable properties
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Algebra.Bundles

    module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where

    import Algebra.Properties.Loop as LoopProperties
    import Algebra.Properties.Quasigroup as QuasigroupProperties
    open import Data.Product.Base using (_,_)
    open import Function.Base using (_$_)
    open import Function.Definitions using (Injective)

    open Group G
    open import Algebra.Consequences.Setoid setoid
    open import Algebra.Definitions _≈_
    open import Algebra.Structures _≈_ using (IsLoop; IsQuasigroup)
    open import Relation.Binary.Reasoning.Setoid setoid

    \\-cong₂ : Congruent₂ _\\_
    \\-cong₂ x≈y u≈v = ∙-cong (⁻¹-cong x≈y) u≈v

    //-cong₂ : Congruent₂ _//_
    //-cong₂ x≈y u≈v = ∙-cong x≈y (⁻¹-cong u≈v)

    ------------------------------------------------------------------------
    -- Groups are quasi-groups

    \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_
    \\-leftDividesˡ x y = begin
      x  ∙ (x \\ y)  ≈⟨ assoc x (x ⁻¹) y ⟨
      x ∙ x ⁻¹ ∙ y   ≈⟨ ∙-congʳ (inverseʳ x) ⟩
      ε ∙ y          ≈⟨ identityˡ y ⟩
      y              ∎

    \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_
    \\-leftDividesʳ x y = begin
      x \\ x ∙ y     ≈⟨ assoc (x ⁻¹) x y ⟨
      x ⁻¹ ∙ x ∙ y   ≈⟨ ∙-congʳ (inverseˡ x) ⟩
      ε ∙ y          ≈⟨ identityˡ y ⟩
      y              ∎

    \\-leftDivides : LeftDivides _∙_ _\\_
    \\-leftDivides = \\-leftDividesˡ , \\-leftDividesʳ

    //-rightDividesˡ : RightDividesˡ _∙_ _//_
    //-rightDividesˡ x y = begin
      (y // x) ∙ x    ≈⟨ assoc y (x ⁻¹) x ⟩
      y ∙ (x ⁻¹ ∙ x)  ≈⟨ ∙-congˡ (inverseˡ x) ⟩
      y ∙ ε           ≈⟨ identityʳ y ⟩
      y               ∎

    //-rightDividesʳ : RightDividesʳ _∙_ _//_
    //-rightDividesʳ x y = begin
      y ∙ x // x    ≈⟨ assoc y x (x ⁻¹) ⟩
      y ∙ (x // x)  ≈⟨ ∙-congˡ (inverseʳ x) ⟩
      y ∙ ε         ≈⟨ identityʳ y ⟩
      y             ∎

    //-rightDivides : RightDivides _∙_ _//_
    //-rightDivides = //-rightDividesˡ , //-rightDividesʳ

    isQuasigroup : IsQuasigroup _∙_ _\\_ _//_
    isQuasigroup = record
      { isMagma = isMagma
      ; \\-cong = \\-cong₂
      ; //-cong = //-cong₂
      ; leftDivides = \\-leftDivides
      ; rightDivides = //-rightDivides
      }

    quasigroup : Quasigroup _ _
    quasigroup = record { isQuasigroup = isQuasigroup }

    open QuasigroupProperties quasigroup public
      using (x≈z//y; y≈x\\z)
      renaming (cancelˡ to ∙-cancelˡ; cancelʳ to ∙-cancelʳ; cancel to ∙-cancel)

    ------------------------------------------------------------------------
    -- Groups are loops

    isLoop : IsLoop _∙_ _\\_ _//_ ε
    isLoop = record { isQuasigroup = isQuasigroup ; identity = identity }

    loop : Loop _ _
    loop = record { isLoop = isLoop }

    open LoopProperties loop public
      using (identityˡ-unique; identityʳ-unique; identity-unique)

    ------------------------------------------------------------------------
    -- Other properties

    inverseˡ-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
    inverseˡ-unique x y eq = trans (x≈z//y x y ε eq) (identityˡ _)

    inverseʳ-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
    inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)

    ε⁻¹≈ε : ε ⁻¹ ≈ ε
    ε⁻¹≈ε = sym $ inverseˡ-unique _ _ (identityˡ ε)

    ⁻¹-selfInverse : SelfInverse _⁻¹
    ⁻¹-selfInverse {x} {y} eq = sym $ inverseˡ-unique x y $ begin
      x ∙ y    ≈⟨ ∙-congˡ eq ⟨
      x ∙ x ⁻¹ ≈⟨ inverseʳ x  ⟩
      ε        ∎

    ⁻¹-involutive : Involutive _⁻¹
    ⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse

    x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y
    x∙y⁻¹≈ε⇒x≈y x y x∙y⁻¹≈ε = begin
      x         ≈⟨ inverseˡ-unique x (y ⁻¹) x∙y⁻¹≈ε ⟩
      y ⁻¹ ⁻¹   ≈⟨ ⁻¹-involutive y ⟩
      y         ∎

    x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε
    x≈y⇒x∙y⁻¹≈ε {x} {y} x≈y = begin
      x ∙ y ⁻¹ ≈⟨ ∙-congʳ x≈y ⟩
      y ∙ y ⁻¹ ≈⟨ inverseʳ y ⟩
      ε        ∎

    ⁻¹-injective : Injective _≈_ _≈_ _⁻¹
    ⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse

    ⁻¹-anti-homo-∙ : ∀ x y → (x ∙ y) ⁻¹ ≈ y ⁻¹ ∙ x ⁻¹
    ⁻¹-anti-homo-∙ x y = ∙-cancelˡ _ _ _ $ begin
      x ∙ y ∙ (x ∙ y) ⁻¹    ≈⟨ inverseʳ _ ⟩
      ε                     ≈⟨ inverseʳ _ ⟨
      x ∙ x ⁻¹              ≈⟨ ∙-congʳ (//-rightDividesʳ y x) ⟨
      (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
      x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎

    ⁻¹-anti-homo-// : ∀ x y → (x // y) ⁻¹ ≈ y // x
    ⁻¹-anti-homo-// x y = begin
      (x // y) ⁻¹      ≡⟨⟩
      (x ∙ y ⁻¹) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
      (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
      y ∙ x ⁻¹         ≡⟨⟩
      y // x ∎

    ⁻¹-anti-homo-\\ : ∀ x y → (x \\ y) ⁻¹ ≈ y \\ x
    ⁻¹-anti-homo-\\ x y = begin
      (x \\ y) ⁻¹      ≡⟨⟩
      (x ⁻¹ ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
      y ⁻¹ ∙ (x ⁻¹) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
      y ⁻¹ ∙ x         ≡⟨⟩
      y \\ x ∎

    \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
    \\≗flip-//⇒comm \\≗//ᵒ x y = begin
      x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨
      x ∙ ((y // x) ∙ x)   ≈⟨ ∙-congˡ (∙-congʳ (\\≗//ᵒ x y)) ⟨
      x ∙ ((x \\ y) ∙ x)   ≈⟨ assoc x (x \\ y) x ⟨
      x ∙ (x \\ y) ∙ x     ≈⟨ ∙-congʳ (\\-leftDividesˡ x y) ⟩
      y ∙ x                ∎

    comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
    comm⇒\\≗flip-// comm x y = begin
      x \\ y    ≡⟨⟩
      x ⁻¹ ∙ y  ≈⟨ comm _ _ ⟩
      y ∙ x ⁻¹  ≡⟨⟩
      y // x    ∎