open import Cat.Univalent
open import Cat.Prelude

open import Data.Dec

module Cat.Instances.Discrete where


# Discrete categories🔗

Given a groupoid $A$, we can build the category ${\mathrm{Disc}}(A)$ with space of objects $A$ and a single morphism $x \to y$ whenever $x \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 $X$ is a discrete type, then it is in particular in Set, and we can make diagrams of shape ${\mathrm{Disc}}(X)$ in some category $\mathcal{C}$, using the decidable equality on $X$. 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′ (el 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 =
Dec-elim (λ _ → 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 \to {\mathrm{Ob}}(\mathcal{C})$, and the decidable equality is used to prove that $f$ respects equality. This is why it’s redundant: $f$ automatically respects equality, because it’s a function! However, by using the decision procedure, we get better computational behaviour: Very often, ${\mathrm{disc}}(x,x)$ will be ${\mathrm{yes}}({\mathrm{refl}})$, and substitution along ${\mathrm{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 $F_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! (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-reflr C refl) ⟩≡
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))