------------------------------------------------------------------------
-- The Agda standard library
--
-- Some basic properties of Loop
------------------------------------------------------------------------

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

open import Algebra.Bundles using (Loop)

module Algebra.Properties.Loop {l₁ l₂} (L : Loop l₁ l₂) where

open Loop L
open import Algebra.Definitions _≈_
open import Algebra.Properties.Quasigroup quasigroup
open import Data.Product.Base using (proj₂)
open import Relation.Binary.Reasoning.Setoid setoid

x//x≈ε :  x  x // x  ε
x//x≈ε x = begin
  x // x       ≈⟨ //-congʳ (identityˡ x) 
  (ε  x) // x ≈⟨ rightDividesʳ x ε 
  ε            

x\\x≈ε :  x  x \\ x  ε
x\\x≈ε x = begin
  x \\ x       ≈⟨ \\-congˡ (identityʳ x ) 
  x \\ (x  ε) ≈⟨ leftDividesʳ x ε 
  ε            

ε\\x≈x :  x  ε \\ x  x
ε\\x≈x x = begin
  ε \\ x       ≈⟨ identityˡ (ε \\ x) 
  ε  (ε \\ x) ≈⟨ leftDividesˡ ε x 
  x            

x//ε≈x :  x  x // ε  x
x//ε≈x x = begin
 x // ε       ≈⟨ identityʳ (x // ε) 
 (x // ε)  ε ≈⟨ rightDividesˡ ε x 
 x            

identityˡ-unique :  x y  x  y  y  x  ε
identityˡ-unique x y eq = begin
  x      ≈⟨ x≈z//y x y y eq 
  y // y ≈⟨ x//x≈ε y 
  ε      

identityʳ-unique :  x y  x  y  x  y  ε
identityʳ-unique x y eq = begin
  y       ≈⟨ y≈x\\z x y x eq 
  x \\ x  ≈⟨ x\\x≈ε x 
  ε       

identity-unique :  {x}  Identity x _∙_  x  ε
identity-unique {x} id = identityˡ-unique x x (proj₂ id x)