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