{-
A group with a with a {left,right}-absorbing is trivial.
Proven jointly with Jule whilst on a walk.
-}

import Level
open import Algebra.Bundles
open import Data.Product using (proj₁ ; proj₂)
import Relation.Binary.Reasoning.Setoid

module abs {c ℓ} (G : Group c ℓ) where

  open Group G
  open Relation.Binary.Reasoning.Setoid setoid

  isRightAbsorbing : Carrier → Set (c Level.⊔ ℓ)
  isRightAbsorbing a = ∀ (x : Carrier) → x ∙ a ≈ a

  isLeftAbsorbing : Carrier → Set (c Level.⊔ ℓ)
  isLeftAbsorbing a = ∀ (x : Carrier) → a ∙ x ≈ a

  rabs-neutral : ∀ (a : Carrier) → isRightAbsorbing a → a ≈ ε
  rabs-neutral a a-rabs = begin
    a ≈⟨ sym (a-rabs (a ⁻¹)) ⟩
    a ⁻¹ ∙ a ≈⟨ inverse .proj₁ a ⟩
    ε ∎

  labs-neutral : ∀ (a : Carrier) → isLeftAbsorbing a → a ≈ ε
  labs-neutral a a-labs = begin
    a ≈⟨ sym (a-labs (a ⁻¹)) ⟩
    a ∙ a ⁻¹ ≈⟨ inverse .proj₂ a ⟩
    ε ∎

  labs-rabs : ∀ (a : Carrier) → isLeftAbsorbing a → isRightAbsorbing a
  labs-rabs a a-labs x = begin
    x ∙ a ≈⟨ ∙-congˡ (labs-neutral a a-labs) ⟩
    x ∙ ε ≈⟨ identityʳ x ⟩
    x ≈⟨ sym (identityˡ x) ⟩
    ε ∙ x ≈⟨ ∙-congʳ (sym (labs-neutral a a-labs)) ⟩
    a ∙ x ≈⟨ a-labs x ⟩
    a ∎

  rabs-is-trivial : ∀ (a : Carrier) → isRightAbsorbing a → ∀ (x : Carrier) → x ≈ ε
  rabs-is-trivial a a-rabs x = begin
    x ≈⟨ sym (identityʳ x) ⟩
    x ∙ ε ≈⟨ ∙-congˡ (sym (rabs-neutral a a-rabs)) ⟩
    (x ∙ a) ≈⟨ a-rabs x ⟩
    a ≈⟨ rabs-neutral a a-rabs ⟩
    ε ∎

  labs-is-trivial : ∀ (a : Carrier) → isLeftAbsorbing a → ∀ (x : Carrier) → x ≈ ε
  labs-is-trivial a a-labs x = rabs-is-trivial a (labs-rabs a a-labs) x