Pregroupoids

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
Imports 
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

Idea

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

Definitions

The predicate on precategories of being a pregroupoid

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

  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)
  where

  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

Properties

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

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

  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} =
    right-unit-law-Σ-is-contr
      ( λ f →
        is-proof-irrelevant-is-prop
          ( 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