{-# OPTIONS --without-K --safe #-}
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
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
abstract
identity : ∀ {x} → id {x = x} ⁻¹ ≡ id
identity =
id ⁻¹ ≡⟨ sym $ right-identity (id ⁻¹) ⟩
id ⁻¹ ∘ id ≡⟨ left-inverse id ⟩∎
id ∎
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 ⁻¹ ∘ p ≡⟨ left-inverse _ ⟩∎
id ∎
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 ⁻¹ ∘_) 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 (_∘ q ⁻¹) p₁∘q≡p₂∘q ⟩
(p₂ ∘ q) ∘ q ⁻¹ ≡⟨ sym $ assoc _ _ _ ⟩
p₂ ∘ (q ∘ q ⁻¹) ≡⟨ cong (_ ∘_) $ right-inverse _ ⟩
p₂ ∘ id ≡⟨ right-identity _ ⟩∎
p₂ ∎
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 ∎
⁻¹∘≡→≡∘ :
∀ {x y z} {p : y ∼ z} {q : x ∼ z} {r : x ∼ y} →
p ⁻¹ ∘ q ≡ r → q ≡ p ∘ r
⁻¹∘≡→≡∘ {p = p} {q = q} {r = r} hyp =
q ≡⟨ sym $ left-identity _ ⟩
id ∘ q ≡⟨ cong (_∘ _) $ sym $ right-inverse _ ⟩
(p ∘ p ⁻¹) ∘ q ≡⟨ sym $ assoc _ _ _ ⟩
p ∘ (p ⁻¹ ∘ q) ≡⟨ cong (_ ∘_) hyp ⟩∎
p ∘ r ∎
⁻¹∘≡id→≡ : ∀ {x y} {p q : x ∼ y} → p ⁻¹ ∘ q ≡ id → q ≡ p
⁻¹∘≡id→≡ {p = p} {q = q} hyp =
q ≡⟨ ⁻¹∘≡→≡∘ hyp ⟩
p ∘ id ≡⟨ right-identity _ ⟩∎
p ∎
⁻¹-bijection : ∀ {x y} → x ∼ y ↔ y ∼ x
⁻¹-bijection = record
{ surjection = record
{ logical-equivalence = record
{ to = _⁻¹
; from = _⁻¹
}
; right-inverse-of = involutive
}
; left-inverse-of = involutive
}