{-# OPTIONS --without-K #-}
module equality.groupoid where

open import equality.core

_⁻¹ : ∀ {i}{X : Set i}{x y : X} → x ≡ y → y ≡ x
_⁻¹ = sym

_⊚_ : ∀ {i}{X : Set i}{x y z : X}
    → x ≡ y → y ≡ z → x ≡ z
_⊚_ = trans
infixl  _⊚_

left-unit : ∀ {i}{X : Set i}{x y : X}
          → (p : x ≡ y)
          → p ⊚ refl ≡ p
left-unit refl = refl

right-unit : ∀ {i}{X : Set i}{x y : X}
           → (p : x ≡ y)
           → refl ⊚ p ≡ p
right-unit refl = refl

associativity : ∀ {i}{X : Set i}{x y z w : X}
              → (p : x ≡ y)(q : y ≡ z)(r : z ≡ w)
              → p ⊚ q ⊚ r ≡ p ⊚ (q ⊚ r)
associativity refl _ _ = refl

left-inverse : ∀ {i}{X : Set i}{x y : X}
             → (p : x ≡ y)
             → p ⊚ p ⁻¹ ≡ refl
left-inverse refl = refl

right-inverse : ∀ {i}{X : Set i}{x y : X}
              → (p : x ≡ y)
              → p ⁻¹ ⊚ p ≡ refl
right-inverse refl = refl