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 _ = β-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
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 β} (disc : Discrete β£ X β£) β (β£ X β£ β Ob C) β Functor (Discβ² X) C Disc-diagram {C = C} {X = X} disc f = F where module C = Precategory C 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 , 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 = map p (disc 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} 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) (X .is-tr _ _ 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! (X .is-tr _ _ _ _) β©β‘ 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))
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-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