```------------------------------------------------------------------------
-- 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

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    ∎
```