open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning as Cat

module Cat.Instances.Discrete.Pre where

Fundamental pregroupoids🔗

module _ where
  open Precategory

If $X$ is a type with no known h-level, we can not directly define a precategory where the type of objects is $X$ and $\mathbf{Hom}(x,y)$ is the type of paths $x\equiv y\text{,}$ since we will not know that this type is a set. However, we can still define an interesting precategory with type of objects $X$ by defining $\mathbf{Hom}(x,y)$ to be the set truncation $\Vert x\equiv y{\Vert }_0\text{.}$

Since under Rezk completion this precategory presents the “path groupoid” of the groupoid truncation $\Vert X{\Vert }_1\text{,}$ we refer to it as the fundamental pregroupoid of $X\text{,}$ and denote it ${\Pi }_1(X)\text{.}$ The naming and notation refers to the fundamental groups of $X\text{.}$ Indeed, if $x:X$ is a point, then the endomorphism space ${\mathbf{Hom}}_{{\Pi }_1(X)}(x,x)$ is exactly the fundamental group ${\pi }_1(X,x)\text{.}$

  Π₁ : ∀ {ℓ} → Type ℓ → Precategory ℓ ℓ
  Π₁ X .Ob          = X
  Π₁ X .Hom     x y = ∥ x ≡ y ∥₀
  Π₁ X .Hom-set x y = hlevel 

  Π₁ X .id      = inc refl
  Π₁ X ._∘_ p q = ⦇ q ∙ p ⦈

  Π₁ X .idr   = elim! λ p     → ap ∥_∥₀.inc (∙-idl p)
  Π₁ X .idl   = elim! λ p     → ap ∥_∥₀.inc (∙-idr p)
  Π₁ X .assoc = elim! λ p q r → ap ∥_∥₀.inc (sym (∙-assoc r q p))

module _ {ℓx o ℓ} {X : Type ℓx} (C : Precategory o ℓ) where
  open Functor
  open Cat C

As for discrete categories, we can extend functions $X\to \mathrm{Ob}(\mathcal{C})$ to functors ${\Pi }_1(X)\to \mathcal{C}\text{.}$ Turning families of objects into diagrams is the primary motivation for the construction of ${\Pi }_1(-)\text{:}$ if $\mathrm{Ob}(\mathcal{C})$ was known to be a groupoid, we could replace $X$ with its groupoid truncation, and use the ordinary “discrete category” construction as the domain of the diagram; but since we will not be able to eliminate $\Vert X{\Vert }_1$ in general, we have to choose a different domain instead.

  Π₁-adjunct₁ : {x y : X} (F : X → ⌞ C ⌟) → ∥ x ≡ y ∥₀ → Hom (F x) (F y)
  Π₁-adjunct₁ F (inc x) = path→iso (ap F x) .to
  Π₁-adjunct₁ F (squash x y p q i j) = Hom-set _ _
    (Π₁-adjunct₁ F x) (Π₁-adjunct₁ F y)
    (λ i → Π₁-adjunct₁ F (p i)) (λ i → Π₁-adjunct₁ F (q i)) i j

  Π₁-adjunct : (X → ⌞ C ⌟) → Functor (Π₁ X) C
  Π₁-adjunct F .F₀   = F
  Π₁-adjunct F .F₁   = Π₁-adjunct₁ F
  Π₁-adjunct F .F-id = transport-refl _
  Π₁-adjunct F .F-∘ {x = x} = elim! λ p q →
    path→iso (ap F (q ∙ p)) .to                     ≡⟨ ap (λ e → subst (Hom (F x)) e id) (ap-∙ F q p) ⟩≡
    path→iso (ap F q ∙ ap F p) .to                  ≡⟨ path→to-∙ C (ap F q) (ap F p) ⟩≡
    (path→iso (ap F p) .to ∘ path→iso (ap F q) .to) ∎