open import 1Lab.HLevel.Closure

open import Cat.Functor.Naturality
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} 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-adjunct
  : βˆ€ ⦃ iss : H-Level {β„“} X 3 ⦄
  β†’ (X β†’ Ob C)
  β†’ Functor (Disc X (hlevel 3)) C
Disc-adjunct = Disc'-adjunct {iss = hlevel 3}

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

open _β‰…_
open Inverses
Disc-natural-iso : βˆ€ {X : Set β„“}
  β†’ {F G : Functor (Disc' X) C}
  β†’ (βˆ€ x β†’ Isomorphism C (F .Fβ‚€ x) (G .Fβ‚€ x))
  β†’ F ≅ⁿ G
Disc-natural-iso isos .to = Disc-natural Ξ» x β†’ isos x .to
Disc-natural-iso isos .from = Disc-natural Ξ» x β†’ isos x .from
Disc-natural-iso isos .inverses = to-inversesⁿ (Ξ» x β†’ isos x .inverses .invl) (Ξ» x β†’ isos x .inverses .invr)