------------------------------------------------------------------------
-- 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 = sym (x≈z//y _ _ _ (identityˡ x))
x\\x≈ε : ∀ x → x \\ x ≈ ε
x\\x≈ε x = sym (y≈x\\z _ _ _ (identityʳ x))
ε\\x≈x : ∀ x → ε \\ x ≈ x
ε\\x≈x x = sym (y≈x\\z _ _ _ (identityˡ x))
x//ε≈x : ∀ x → x // ε ≈ x
x//ε≈x x = sym (x≈z//y _ _ _ (identityʳ 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)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4