module Cat.Instances.Discrete where

Discrete categoriesπŸ”—

Given a groupoid AA, we can build the category Disc(A)\mathrm{Disc}(A) with space of objects AA and a single morphism xβ†’yx \to y whenever x≑yx \equiv y.

Disc : (A : Type β„“) β†’ is-groupoid A β†’ Precategory β„“ β„“
Disc A A-grpd .Ob = A
Disc A A-grpd .Hom = _≑_
Disc A A-grpd .Hom-set = A-grpd
Disc A A-grpd .id = refl
Disc A A-grpd ._∘_ p q = q βˆ™ p
Disc A A-grpd .idr _ = βˆ™-idl _
Disc A A-grpd .idl _ = βˆ™-idr _
Disc A A-grpd .assoc _ _ _ = sym (βˆ™-assoc _ _ _)

Disc' : Set β„“ β†’ Precategory β„“ β„“
Disc' A = Disc ∣ A ∣ h where abstract
  h : is-groupoid ∣ A ∣
  h = is-hlevel-suc 2 (A .is-tr)

Clearly this is a univalent groupoid:

Disc-is-category : βˆ€ {A : Type β„“} {A-grpd} β†’ is-category (Disc A A-grpd)
Disc-is-category .to-path is = is .to
Disc-is-category .to-path-over is = β‰…-pathp _ _ _ Ξ» i j β†’ is .to (i ∧ j)

Disc-is-groupoid : βˆ€ {A : Type β„“} {A-grpd} β†’ is-pregroupoid (Disc A A-grpd)
Disc-is-groupoid p = make-invertible _ (sym p) (βˆ™-invl p) (βˆ™-invr p)

We can lift any function between the underlying types to a functor between discrete categories. This is because every function automatically respects equality in a functorial way.

lift-disc
  : βˆ€ {A : Set β„“} {B : Set β„“'}
  β†’ (∣ A ∣ β†’ ∣ B ∣)
  β†’ Functor (Disc' A) (Disc' B)
lift-disc f .Fβ‚€ = f
lift-disc f .F₁ = ap f
lift-disc f .F-id = refl
lift-disc f .F-∘ p q = ap-βˆ™ f q p

Diagrams in Disc(X)πŸ”—

If XX is a discrete type, then it is in particular in Set, and we can make diagrams of shape Disc(X)\mathrm{Disc}(X) in some category C\mathcal{C}, using the decidable equality on XX. We note that the decidable equality is redundant information: The construction Disc' above extends into a left adjoint to the Ob functor.

Disc-diagram
  : βˆ€ {X : Set β„“} ⦃ _ : Discrete ∣ X ∣ ⦄
  β†’ (∣ X ∣ β†’ Ob C)
  β†’ Functor (Disc' X) C
Disc-diagram {C = C} {X = X} ⦃ d ⦄ f = F where
  module C = Precategory C

  P : ∣ X ∣ β†’ ∣ X ∣ β†’ Type _
  P x y = C.Hom (f x) (f y)

  go : βˆ€ {x y : ∣ X ∣} β†’ x ≑ y β†’ Dec (x ≑ᡒ y) β†’ P x y
  go {x} {.x} p (yes reflα΅’) = C.id
  go {x} {y}  p (no Β¬p)     = absurd (Β¬p (Id≃path.from p))

The object part of the functor is the provided f:Xβ†’Ob(C)f : X \to \mathrm{Ob}(\mathcal{C}), and the decidable equality is used to prove that ff respects equality. This is why it’s redundant: ff automatically respects equality, because it’s a function! However, by using the decision procedure, we get better computational behaviour: Very often, disc(x,x)\mathrm{disc}(x,x) will be yes(refl)\mathrm{yes}(\mathrm{refl}), and substitution along refl\mathrm{refl} is easy to deal with.

  F : Functor _ _
  F .Fβ‚€ = f
  F .F₁ {x} {y} p = go p (x ≑ᡒ? y)

Proving that our our F1F_1 is functorial involves a bunch of tedious computations with equalities and a whole waterfall of absurd cases:

  F .F-id {x} = refl
  F .F-∘  {x} {y} {z} f g =
    J (Ξ» y g β†’ βˆ€ {z} (f : y ≑ z) β†’ go (g βˆ™ f) (x ≑ᡒ? z) ≑ go f (y ≑ᡒ? z) C.∘ go g (x ≑ᡒ? y))
      (Ξ» f β†’ J (Ξ» z f β†’ go (refl βˆ™ f) (x ≑ᡒ? z) ≑ go f (x ≑ᡒ? z) C.∘ C.id) (sym (C.idr _)) f)
      g f