Direct proof for groupoidal structure of homotopic identity types via path induction in Agda

groupoid.agda

{-# OPTIONS --without-K #-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

pattern erefl x = refl {x = x}


--- path induction ---
J : ∀ {A : Set} →
    ∀ (C : ∀ (x y : A) → x ≡ y → Set) →
        (∀ (x : A) → C x x refl) →
        (∀ (x y : A) → ∀ (p : x ≡ y) → C x y p)
J {A} C c x x refl = c x


--- identity types form a groupoid ---
_∙_ : ∀ {A : Set} {x y z : A} →
    x ≡ y → y ≡ z → x ≡ z
_∙_ {_} {x} {y} {z} p = J (λ a b p → (b ≡ z → a ≡ z)) (λ a p → p) x y p

_⁻¹ : ∀ {A : Set} {x y : A} →
    x ≡ y → y ≡ x
_⁻¹ {_} {x} {y} p = J (λ a b _ → b ≡ a) (λ x → erefl x) x y p


infixr 80 _∙_
infixr 100 _⁻¹



refl∙refl : ∀ {A : Set} {x : A} →
    (erefl x ∙ erefl x) ≡ erefl x
refl∙refl {_} {x} = erefl (erefl x)

∙-refl : ∀ {A : Set} {x y : A} {p : x ≡ y} →
    p ∙ erefl y ≡ p
∙-refl {_} {x} {y} {p} = J (λ a b q → q ∙ erefl b ≡ q) (λ a → refl∙refl) x y p

refl-∙ : ∀ {A : Set} {x y : A} {p : x ≡ y} →
    erefl x ∙ p ≡ p
refl-∙ {_} {x} {y} {p} = J (λ a b q → erefl a ∙ q ≡ q) (λ a → refl∙refl) x y p



∙-⁻¹ : ∀ {A : Set} {x y : A} {p : x ≡ y} →
    p ∙ (p ⁻¹) ≡ erefl x
∙-⁻¹ {_} {x} {y} {p} = J (λ a b q → q ∙ (q ⁻¹) ≡ erefl a) (λ a → refl∙refl) x y p

⁻¹-∙ : ∀ {A : Set} {x y : A} {p : x ≡ y} →
    (p ⁻¹) ∙ p ≡ erefl y
⁻¹-∙ {_} {x} {y} {p} = J (λ a b q → (q ⁻¹) ∙ q ≡ erefl b) (λ a → refl∙refl) x y p



⁻¹⁻¹ : ∀ {A : Set} {x y : A} {p : x ≡ y} →
    (p ⁻¹) ⁻¹ ≡ p
⁻¹⁻¹ {_} {x} {y} {p} = J (λ a b q → (q ⁻¹) ⁻¹ ≡ q) (λ a → erefl (erefl a)) x y p



∙-assoc : ∀ {A : Set} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
    (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
∙-assoc {A} {w} {x} {y} {z} p q r = (J
    (λ w' x' p' → ∀ (y' z' : A) (q' : x' ≡ y') (r' : y' ≡ z') → ((p' ∙ q') ∙ r' ≡ p' ∙ (q' ∙ r')))
    (λ w' y' z' q' r' → erefl (q' ∙ r')) w x p) y z q r