------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra using (MoufangLoop)
module Algebra.Properties.MoufangLoop {a ℓ} (M : MoufangLoop a ℓ) where
open MoufangLoop M
open import Algebra.Definitions _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Data.Product.Base using (_,_)
alternativeˡ : LeftAlternative _∙_
alternativeˡ x y = begin
(x ∙ x) ∙ y ≈⟨ ∙-congʳ (∙-congˡ (sym (identityˡ x))) ⟩
(x ∙ (ε ∙ x)) ∙ y ≈⟨ sym (leftBol x ε y) ⟩
x ∙ (ε ∙ (x ∙ y)) ≈⟨ ∙-congˡ (identityˡ ((x ∙ y))) ⟩
x ∙ (x ∙ y) ∎
alternativeʳ : RightAlternative _∙_
alternativeʳ x y = begin
x ∙ (y ∙ y) ≈⟨ ∙-congˡ(∙-congʳ(sym (identityʳ y))) ⟩
x ∙ ((y ∙ ε) ∙ y) ≈⟨ sym (rightBol y ε x) ⟩
((x ∙ y) ∙ ε ) ∙ y ≈⟨ ∙-congʳ (identityʳ ((x ∙ y))) ⟩
(x ∙ y) ∙ y ∎
alternative : Alternative _∙_
alternative = alternativeˡ , alternativeʳ
flex : Flexible _∙_
flex x y = begin
(x ∙ y) ∙ x ≈⟨ ∙-congˡ (sym (identityˡ x)) ⟩
(x ∙ y) ∙ (ε ∙ x) ≈⟨ identical y ε x ⟩
x ∙ ((y ∙ ε) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (identityʳ y)) ⟩
x ∙ (y ∙ x) ∎
z∙xzy≈zxz∙y : ∀ x y z → (z ∙ (x ∙ (z ∙ y))) ≈ (((z ∙ x) ∙ z) ∙ y)
z∙xzy≈zxz∙y x y z = sym (begin
((z ∙ x) ∙ z) ∙ y ≈⟨ (∙-congʳ (flex z x )) ⟩
(z ∙ (x ∙ z)) ∙ y ≈⟨ sym (leftBol z x y) ⟩
z ∙ (x ∙ (z ∙ y)) ∎)
x∙zyz≈xzy∙z : ∀ x y z → (x ∙ (z ∙ (y ∙ z))) ≈ (((x ∙ z) ∙ y) ∙ z)
x∙zyz≈xzy∙z x y z = begin
x ∙ (z ∙ (y ∙ z)) ≈⟨ (∙-congˡ (sym (flex z y ))) ⟩
x ∙ ((z ∙ y) ∙ z) ≈⟨ sym (rightBol z y x) ⟩
((x ∙ z) ∙ y) ∙ z ∎
z∙xyz≈zxy∙z : ∀ x y z → (z ∙ ((x ∙ y) ∙ z)) ≈ ((z ∙ (x ∙ y)) ∙ z)
z∙xyz≈zxy∙z x y z = sym (flex z (x ∙ y))
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