open import Cat.Univalent
open import Cat.Prelude

module Cat.Instances.Discrete where

Discrete categoriesπŸ”—

Given a groupoid AA, we can build the category Disc(A)\id{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 _ = βˆ™-id-l _
Disc A A-grpd .idl _ = βˆ™-id-r _
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)

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-comp-path 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)\id{Disc}(X) in some category C\ca{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
  : βˆ€ {iss : is-set X} (disc : Discrete X)
  β†’ (X β†’ Ob C)
  β†’ Functor (Discβ€² (X , iss)) C
Disc-diagram {X = X} {C = C} disc f = F where
  module C = Precategory C
  set : is-set X
  set = Discrete→is-set disc

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

  map : βˆ€ {x y : X} β†’ x ≑ y β†’ Dec (x ≑ y) β†’ P x y
  map {x} {y} p =
    case (Ξ» _ β†’ P x y)
         (Ξ» q β†’ subst (P x) q C.id)
         (Ξ» Β¬p β†’ absurd (Β¬p p))

The object part of the functor is the provided f:Xβ†’Ob(C)f : X \to \id{Ob}(\ca{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)\id{disc}(x,x) will be yes(refl)\id{yes}(\id{refl}), and substitution along refl\id{refl} is easy to deal with.

  F : Functor _ _
  F .Fβ‚€ = f
  F .F₁ {x} {y} p = map p (disc 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} with inspect (disc x x)
  ... | yes p , q =
    map refl (disc x x)   β‰‘βŸ¨ ap (map refl) q βŸ©β‰‘
    map refl (yes p)      β‰‘βŸ¨ ap (map refl βŠ™ yes) (set _ _ p refl) βŸ©β‰‘
    map refl (yes refl)   β‰‘βŸ¨βŸ©
    subst (P x) refl C.id β‰‘βŸ¨ transport-refl _ βŸ©β‰‘
    C.id                  ∎
  ... | no Β¬x≑x , _ = absurd (Β¬x≑x refl)

  F .F-∘ {x} {y} {z} f g with inspect (disc x y) | inspect (disc x z) | inspect (disc y z)
  ... | yes x=y , p1 | yes x=z , p2 | yes y=z , p3 =
    map (g βˆ™ f) (disc x z)                 β‰‘βŸ¨ ap (map (g βˆ™ f)) p2 βŸ©β‰‘
    map (g βˆ™ f) (yes x=z)                  β‰‘βŸ¨ ap (map (g βˆ™ f) βŠ™ yes) (set _ _ _ _) βŸ©β‰‘
    map (g βˆ™ f) (yes (x=y βˆ™ y=z))          β‰‘βŸ¨βŸ©
    subst (P x) (x=y βˆ™ y=z) C.id           β‰‘βŸ¨ subst-βˆ™ (P x) _ _ _ βŸ©β‰‘
    subst (P x) y=z (subst (P _) x=y C.id) β‰‘βŸ¨ from-pathp ((Hom-pathp C (apβ‚‚ C._∘_ refl (apβ‚‚ C._∘_ refl (transport-refl _) βˆ™ C.idr _)))) βŸ©β‰‘
    map f (yes y=z) C.∘ map g (yes x=y)    β‰‘Λ˜βŸ¨ apβ‚‚ C._∘_ (ap (map f) p3) (ap (map g) p1) βŸ©β‰‘Λ˜
    map f (disc y z) C.∘ map g (disc x y)  ∎

  ... | yes x=y , _ | yes x=z , _ | no  y≠z , _ = absurd (y≠z f)
  ... | yes x=y , _ | no  xβ‰ z , _ | yes y=z , _ = absurd (xβ‰ z (g βˆ™ f))
  ... | yes x=y , _ | no  xβ‰ z , _ | no  yβ‰ z , _ = absurd (xβ‰ z (g βˆ™ f))
  ... | no x≠y , _  | yes x=z , _ | yes y=z , _ = absurd (x≠y g)
  ... | no x≠y , _  | yes x=z , _ | no  y≠z , _ = absurd (y≠z f)
  ... | no xβ‰ y , _  | no  xβ‰ z , _ | yes y=z , _ = absurd (xβ‰ z (g βˆ™ f))
  ... | no xβ‰ y , _  | no  xβ‰ z , _ | no  yβ‰ z , _ = absurd (xβ‰ z (g βˆ™ f))