{-# OPTIONS --safe --without-K #-} module Algebra.Structure.PartialMonoid where open import Level open import Algebra.Core open import Data.Product hiding (assocˡ; assocʳ) open import Relation.Binary open import Relation.Binary.PropositionalEquality using (subst; dcong₂; _≡_) record IsPartialMonoid {a b c} {A : Set a} (_≈_ : Rel A b) (_R_ : Rel A c) (∙ : (x y : A) → x R y → A) (ε : A) : Set (a ⊔ b ⊔ c) where private ∙[_] : {x y : A} → x R y → A ∙[_] {x} {y} xy = ∙ x y xy field isEquivalence : IsEquivalence _≈_ A-set : Irrelevant (_≡_ {A = A}) R-prop : Irrelevant _R_ ε-compatˡ : ∀ {x} → ε R x ε-compatʳ : ∀ {x} → x R ε identityˡ : ∀ {x} → ∙[ ε-compatˡ {x} ] ≈ x identityʳ : ∀ {x} → ∙[ ε-compatʳ {x} ] ≈ x assocˡ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → Σ[ xy ∈ x R y ] Σ[ q ∈ ∙[ xy ] R z ] (∙[ p ] ≈ ∙[ q ]) assocʳ : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → Σ[ yz ∈ y R z ] Σ[ q ∈ x R ∙[ yz ] ] (∙[ p ] ≈ ∙[ q ]) assocL1 : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → Σ[ xy ∈ x R y ] (∙[ xy ] R z) assocL1 yz p = let (a , b , _) = assocˡ yz p in a , b assocR1 : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → Σ[ yz ∈ y R z ] (x R ∙[ yz ]) assocR1 yz p = let (a , b , _) = assocʳ yz p in a , b identityˡ' : ∀ {x} (r : ε R x) → ∙[ r ] ≈ x identityˡ' {x} r = subst (λ z → ∙[ z ] ≈ x) (R-prop ε-compatˡ r) identityˡ identityʳ' : ∀ {x} (r : x R ε) → ∙[ r ] ≈ x identityʳ' {x} r = subst (λ z → ∙[ z ] ≈ x) (R-prop ε-compatʳ r) identityʳ assocˡ₁ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → x R y assocˡ₁ yz p = let (a , b , _) = assocˡ yz p in a assocˡ₃ : ∀ {x y z} → (yz : y R z) → (p : x R (∙[ yz ])) → (xy : x R y) → (q : ∙[ xy ] R z ) → (∙ x (∙ y z yz) p ≈ ∙ (∙ x y xy) z q) assocˡ₃ {x} {y} {z} yx p xy q = subst (λ w → ∙ x (∙ y z yx) p ≈ ∙ (∙ x y (proj₁ w)) z (proj₂ w)) goal (proj₂ (proj₂ (assocˡ yx p))) where goal : (proj₁ (assocˡ yx p) , proj₁ (proj₂ (assocˡ yx p))) ≡ (xy , q) goal = dcong₂ _,_ (R-prop _ xy) (R-prop _ q) assocʳ₃ : ∀ {x y z} → (xy : x R y) → (p : ∙[ xy ] R z) → (yz : y R z) (q : x R ∙[ yz ]) → (∙[ p ] ≈ ∙[ q ]) assocʳ₃ {x} {y} {z} yx p xy q = subst (λ w → ∙ (∙ x y yx) z p ≈ ∙ x (∙ y z (proj₁ w)) (proj₂ w)) goal (proj₂ (proj₂ (assocʳ yx p))) where goal : (proj₁ (assocʳ yx p) , proj₁ (proj₂ (assocʳ yx p))) ≡ (xy , q) goal = dcong₂ _,_ (R-prop _ xy) (R-prop _ q) record IsReflexivePartialMonoid {a b c} {A : Set a} (_≈_ : Rel A b) (_R_ : Rel A c) (∙ : (x y : A) → x R y → A) (ε : A) : Set (a ⊔ b ⊔ c) where field isPMon : IsPartialMonoid _≈_ _R_ ∙ ε reflexive : ∀ {x} → x R x open IsPartialMonoid isPMon public