module Cat.Instances.Discrete where

Discrete categoriesπŸ”—

Given a groupoid we can build the category with space of objects and a single morphism whenever 

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 is a discrete type, then it is in particular in Set, and we can make diagrams of shape in some category using the decidable equality on 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 and the decidable equality is used to prove that respects equality. This is why it’s redundant: automatically respects equality, because it’s a function! However, by using the decision procedure, we get better computational behaviour: Very often, will be and substitution along is easy to deal with.

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

Proving that our our 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