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 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
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 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
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