{-# OPTIONS --without-K --safe #-}
module Categories.Category.Groupoid where
 
open import Level using (Level; suc; _⊔_)
 
open import Categories.Category
import Categories.Morphism
 
record IsGroupoid {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C public
  open Definitions C public
 
  open Categories.Morphism C
 
  infix  _⁻¹
 
  field
    _⁻¹ : ∀ {A B} → A ⇒ B → B ⇒ A
    iso : ∀ {A B} {f : A ⇒ B} → Iso f (f ⁻¹)
 
  module iso {A B f} = Iso (iso {A} {B} {f})
 
  equiv-obj : ∀ {A B} → A ⇒ B → A ≅ B
  equiv-obj f = record
    { from = f
    ; to   = _
    ; iso  = iso
    }
 
  -- this definition doesn't seem to 'carry its weight'
  equiv-obj-sym : ∀ {A B} → A ⇒ B → B ≅ A
  equiv-obj-sym f = ≅.sym (equiv-obj f)
 
-- A groupoid is a category that has a groupoid structure
 
record Groupoid (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    category   : Category o ℓ e
    isGroupoid : IsGroupoid category
 
  open IsGroupoid isGroupoid public