123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657-------------------------------------------------------------------------- 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 Lopen import Algebra.Definitions _≈_open import Algebra.Properties.Quasigroup quasigroupopen 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 // ε ≈ xx//ε≈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)