{-# 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