------------------------------------------------------------------------ -- Groupoids ------------------------------------------------------------------------ {-# OPTIONS --without-K #-} open import Equality module Groupoid {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where open import Prelude hiding (id; _∘_) open import Bijection eq hiding (id; _∘_) open Derived-definitions-and-properties eq -- Groupoids using _≡_ as the underlying equality. record Groupoid o p : Set (lsuc (o ⊔ p)) where infix 8 _⁻¹ infixr 7 _∘_ infix 4 _∼_ field Object : Set o _∼_ : Object → Object → Set p id : ∀ {x} → x ∼ x _∘_ : ∀ {x y z} → y ∼ z → x ∼ y → x ∼ z _⁻¹ : ∀ {x y} → x ∼ y → y ∼ x left-identity : ∀ {x y} (p : x ∼ y) → id ∘ p ≡ p right-identity : ∀ {x y} (p : x ∼ y) → p ∘ id ≡ p assoc : ∀ {w x y z} (p : y ∼ z) (q : x ∼ y) (r : w ∼ x) → p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r left-inverse : ∀ {x y} (p : x ∼ y) → p ⁻¹ ∘ p ≡ id right-inverse : ∀ {x y} (p : x ∼ y) → p ∘ p ⁻¹ ≡ id -- Note that this definition should perhaps contain more coherence -- properties: we have not assumed that _≡_ is proof-irrelevant. -- Some derived properties. abstract -- The identity is an identity for the inverse operator as well. identity : ∀ {x} → id {x = x} ⁻¹ ≡ id identity = id ⁻¹ ≡⟨ sym \$ right-identity (id ⁻¹) ⟩ id ⁻¹ ∘ id ≡⟨ left-inverse id ⟩∎ id ∎ -- If p is idempotent with respect to _∘_, then p is equal to the -- identity element. idempotent⇒≡id : ∀ {x} {p : x ∼ x} → p ∘ p ≡ p → p ≡ id idempotent⇒≡id {p = p} p∘p≡p = p ≡⟨ sym \$ left-identity _ ⟩ id ∘ p ≡⟨ cong (_∘ _) \$ sym \$ left-inverse _ ⟩ (p ⁻¹ ∘ p) ∘ p ≡⟨ sym \$ assoc _ _ _ ⟩ p ⁻¹ ∘ (p ∘ p) ≡⟨ cong (_ ∘_) p∘p≡p ⟩ p ⁻¹ ∘ p ≡⟨ left-inverse _ ⟩∎ id ∎ -- Groupoids are left-cancellative and right-cancellative. left-cancellative : ∀ {x y z} {p : y ∼ z} {q₁ q₂ : x ∼ y} → p ∘ q₁ ≡ p ∘ q₂ → q₁ ≡ q₂ left-cancellative {p = p} {q₁} {q₂} p∘q₁≡p∘q₂ = q₁ ≡⟨ sym \$ left-identity _ ⟩ id ∘ q₁ ≡⟨ cong (_∘ _) \$ sym \$ left-inverse _ ⟩ (p ⁻¹ ∘ p) ∘ q₁ ≡⟨ sym \$ assoc _ _ _ ⟩ p ⁻¹ ∘ (p ∘ q₁) ≡⟨ cong (_ ∘_) p∘q₁≡p∘q₂ ⟩ p ⁻¹ ∘ (p ∘ q₂) ≡⟨ assoc _ _ _ ⟩ (p ⁻¹ ∘ p) ∘ q₂ ≡⟨ cong (_∘ _) \$ left-inverse _ ⟩ id ∘ q₂ ≡⟨ left-identity _ ⟩∎ q₂ ∎ right-cancellative : ∀ {x y z} {p₁ p₂ : y ∼ z} {q : x ∼ y} → p₁ ∘ q ≡ p₂ ∘ q → p₁ ≡ p₂ right-cancellative {p₁ = p₁} {p₂} {q} p₁∘q≡p₂∘q = p₁ ≡⟨ sym \$ right-identity _ ⟩ p₁ ∘ id ≡⟨ cong (_ ∘_) \$ sym \$ right-inverse _ ⟩ p₁ ∘ (q ∘ q ⁻¹) ≡⟨ assoc _ _ _ ⟩ (p₁ ∘ q) ∘ q ⁻¹ ≡⟨ cong (_∘ _) p₁∘q≡p₂∘q ⟩ (p₂ ∘ q) ∘ q ⁻¹ ≡⟨ sym \$ assoc _ _ _ ⟩ p₂ ∘ (q ∘ q ⁻¹) ≡⟨ cong (_ ∘_) \$ right-inverse _ ⟩ p₂ ∘ id ≡⟨ right-identity _ ⟩∎ p₂ ∎ -- The inverse operator is involutive. involutive : ∀ {x y} (p : x ∼ y) → p ⁻¹ ⁻¹ ≡ p involutive p = p ⁻¹ ⁻¹ ≡⟨ sym \$ right-identity (p ⁻¹ ⁻¹) ⟩ p ⁻¹ ⁻¹ ∘ id ≡⟨ sym \$ cong (_∘_ (p ⁻¹ ⁻¹)) (left-inverse p) ⟩ p ⁻¹ ⁻¹ ∘ (p ⁻¹ ∘ p) ≡⟨ assoc _ _ _ ⟩ (p ⁻¹ ⁻¹ ∘ p ⁻¹) ∘ p ≡⟨ cong (λ q → q ∘ p) (left-inverse (p ⁻¹)) ⟩ id ∘ p ≡⟨ left-identity p ⟩∎ p ∎ -- The inverse operator is a bijection. ⁻¹-bijection : ∀ {x y} → x ∼ y ↔ y ∼ x ⁻¹-bijection = record { surjection = record { logical-equivalence = record { to = _⁻¹ ; from = _⁻¹ } ; right-inverse-of = involutive } ; left-inverse-of = involutive }