open import Cat.Instances.Product
open import Cat.Groupoid
open import Cat.Morphism
open import Cat.Prelude

open import Data.Id.Base
open import Data.Dec

import Cat.Reasoning
module Cat.Instances.Discrete where
private variable
  β„“ β„“' : Level
  X : Type β„“
  C : Precategory β„“ β„“'

open Precategory
open Functor
open _=>_

Discrete categoriesπŸ”—

Given a groupoid we can see as a category with space of objects and path types as When is a set, we call this the discrete category on 

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)

By construction, 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
Codisc' : βˆ€ {β„“'} β†’ Type β„“ β†’ Precategory β„“ β„“'
Codisc' x .Ob = x
Codisc' x .Hom _ _ = Lift _ ⊀
Codisc' x .Hom-set _ _ = is-prop→is-set (λ _ _ i → lift tt)
Codisc' x .id = lift tt
Codisc' x ._∘_ _ _ = lift tt
Codisc' x .idr _ = refl
Codisc' x .idl _ = refl
Codisc' x .assoc _ _ _ = refl

Diagrams in Disc(X)πŸ”—

If is a discrete type, then it is in particular a set, and we can make diagrams of shape in some category using the decidable equality on to improve computation. We note that the decidable equality is superfluous 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
Disc-adjunct
  : βˆ€ {iss : is-groupoid X}
  β†’ (X β†’ Ob C)
  β†’ Functor (Disc X iss) C
Disc-adjunct {C = C} F .Fβ‚€ = F
Disc-adjunct {C = C} F .F₁ p = subst (C .Hom (F _) βŠ™ F) p (C .id)
Disc-adjunct {C = C} F .F-id = transport-refl _
Disc-adjunct {C = C} {iss = iss} F .F-∘ {x} {y} {z} f g = path where
  import Cat.Reasoning C as C
  go = Disc-adjunct {C = C} {iss} F .F₁
  abstract
    path : go (g βˆ™ f) ≑ C ._∘_ (go f) (go g)
    path =
      J' (Ξ» y z f β†’ βˆ€ {x} (g : x ≑ y) β†’ go (g βˆ™ f) ≑ go f C.∘ go g)
        (Ξ» x g β†’ subst-βˆ™ (C .Hom (F _) βŠ™ F) _ _ _
              βˆ™βˆ™ transport-refl _
              βˆ™βˆ™ C.introl (transport-refl _))
        f {x} g

Disc-into
  : βˆ€ {β„“} (X : Set β„“)
  β†’ (F : C .Ob β†’ ∣ X ∣)
  β†’ (F₁ : βˆ€ {x y} β†’ C .Hom x y β†’ F x ≑ F y)
  β†’ Functor C (Disc' X)
Disc-into X F F₁ .Fβ‚€ = F
Disc-into X F F₁ .F₁ = F₁
Disc-into X F F₁ .F-id = X .is-tr _ _ _ _
Disc-into X F F₁ .F-∘ _ _ = X .is-tr _ _ _ _
Disc-natural
  : βˆ€ {X : Set β„“}
  β†’ {F G : Functor (Disc' X) C}
  β†’ (βˆ€ x β†’ C .Hom (F .Fβ‚€ x) (G .Fβ‚€ x))
  β†’ F => G
Disc-natural fam .Ξ· = fam
Disc-natural {C = C} {F = F} {G = G} fam .is-natural x y f =
  J (Ξ» y p β†’ fam y C.∘ F .F₁ p ≑ G .F₁ p C.∘ fam x)
    (C.elimr (F .F-id) βˆ™ C.introl (G .F-id))
    f
  where module C = Cat.Reasoning C

Disc-naturalβ‚‚
  : βˆ€ {X : Type β„“} {Y : Type β„“'}
  β†’ {issx : is-groupoid X} {issy : is-groupoid Y}
  β†’ {F G : Functor (Disc X issx Γ—αΆœ Disc Y issy) C}
  β†’ ((x : X Γ— Y) β†’ C .Hom (F .Fβ‚€ x) (G .Fβ‚€ x))
  β†’ F => G
Disc-naturalβ‚‚ fam .Ξ· = fam
Disc-naturalβ‚‚ {C = C} {F = F} {G = G} fam .is-natural x y (p , q) =
  J (Ξ» y' p' β†’ fam y' C.∘ F .F₁ (ap fst p' , ap snd p')
             ≑ G .F₁ (ap fst p' , ap snd p') C.∘ fam x)
    (C.elimr (F .F-id) βˆ™ C.introl (G .F-id))
    (Ξ£-pathp p q)
  where module C = Cat.Reasoning C