Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-09-21.
Last modified on 2024-03-11.

module category-theory.pregroupoids where
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels


A pregroupoid is a precategory in which every morphism is an isomorphism.


The predicate on precategories of being a pregroupoid

module _
  {l1 l2 : Level} (C : Precategory l1 l2)

  is-pregroupoid-Precategory : UU (l1  l2)
  is-pregroupoid-Precategory =
    (x y : obj-Precategory C) (f : hom-Precategory C x y) 
    is-iso-Precategory C f

  is-prop-is-pregroupoid-Precategory : is-prop is-pregroupoid-Precategory
  is-prop-is-pregroupoid-Precategory =
    is-prop-iterated-Π 3  x y  is-prop-is-iso-Precategory C)

  is-pregroupoid-prop-Precategory : Prop (l1  l2)
  pr1 is-pregroupoid-prop-Precategory = is-pregroupoid-Precategory
  pr2 is-pregroupoid-prop-Precategory = is-prop-is-pregroupoid-Precategory

The type of pregroupoids

Pregroupoid :
  (l1 l2 : Level)  UU (lsuc l1  lsuc l2)
Pregroupoid l1 l2 = Σ (Precategory l1 l2) (is-pregroupoid-Precategory)

module _
  {l1 l2 : Level} (G : Pregroupoid l1 l2)

  precategory-Pregroupoid : Precategory l1 l2
  precategory-Pregroupoid = pr1 G

  is-pregroupoid-Pregroupoid :
    is-pregroupoid-Precategory precategory-Pregroupoid
  is-pregroupoid-Pregroupoid = pr2 G

  obj-Pregroupoid : UU l1
  obj-Pregroupoid = obj-Precategory precategory-Pregroupoid

  hom-set-Pregroupoid : obj-Pregroupoid  obj-Pregroupoid  Set l2
  hom-set-Pregroupoid = hom-set-Precategory precategory-Pregroupoid

  hom-Pregroupoid : obj-Pregroupoid  obj-Pregroupoid  UU l2
  hom-Pregroupoid = hom-Precategory precategory-Pregroupoid

  id-hom-Pregroupoid :
    {x : obj-Pregroupoid}  hom-Pregroupoid x x
  id-hom-Pregroupoid = id-hom-Precategory precategory-Pregroupoid

  comp-hom-Pregroupoid :
    {x y z : obj-Pregroupoid}  hom-Pregroupoid y z 
    hom-Pregroupoid x y  hom-Pregroupoid x z
  comp-hom-Pregroupoid = comp-hom-Precategory precategory-Pregroupoid

  associative-comp-hom-Pregroupoid :
    {x y z w : obj-Pregroupoid} (h : hom-Pregroupoid z w)
    (g : hom-Pregroupoid y z) (f : hom-Pregroupoid x y) 
    comp-hom-Pregroupoid (comp-hom-Pregroupoid h g) f 
    comp-hom-Pregroupoid h (comp-hom-Pregroupoid g f)
  associative-comp-hom-Pregroupoid =
    associative-comp-hom-Precategory precategory-Pregroupoid

  involutive-eq-associative-comp-hom-Pregroupoid :
    {x y z w : obj-Pregroupoid} (h : hom-Pregroupoid z w)
    (g : hom-Pregroupoid y z) (f : hom-Pregroupoid x y) 
    comp-hom-Pregroupoid (comp-hom-Pregroupoid h g) f =ⁱ
    comp-hom-Pregroupoid h (comp-hom-Pregroupoid g f)
  involutive-eq-associative-comp-hom-Pregroupoid =
    involutive-eq-associative-comp-hom-Precategory precategory-Pregroupoid

  left-unit-law-comp-hom-Pregroupoid :
    {x y : obj-Pregroupoid} (f : hom-Pregroupoid x y) 
    ( comp-hom-Pregroupoid id-hom-Pregroupoid f)  f
  left-unit-law-comp-hom-Pregroupoid =
    left-unit-law-comp-hom-Precategory precategory-Pregroupoid

  right-unit-law-comp-hom-Pregroupoid :
    {x y : obj-Pregroupoid} (f : hom-Pregroupoid x y) 
    ( comp-hom-Pregroupoid f id-hom-Pregroupoid)  f
  right-unit-law-comp-hom-Pregroupoid =
    right-unit-law-comp-hom-Precategory precategory-Pregroupoid

  iso-Pregroupoid : (x y : obj-Pregroupoid)  UU l2
  iso-Pregroupoid = iso-Precategory precategory-Pregroupoid


The type of isomorphisms in a pregroupoid is equivalent to the type of morphisms

module _
  {l1 l2 : Level} (G : Pregroupoid l1 l2)

  inv-compute-iso-Pregroupoid :
    {x y : obj-Pregroupoid G}  iso-Pregroupoid G x y  hom-Pregroupoid G x y
  inv-compute-iso-Pregroupoid {x} {y} =
      ( λ f 
          ( is-prop-is-iso-Precategory (precategory-Pregroupoid G) f)
          ( is-pregroupoid-Pregroupoid G x y f))

  compute-iso-Pregroupoid :
    {x y : obj-Pregroupoid G}  hom-Pregroupoid G x y  iso-Pregroupoid G x y
  compute-iso-Pregroupoid = inv-equiv inv-compute-iso-Pregroupoid

See also

Recent changes