module Cat.Functor.Concrete where

Concrete categoriesπŸ”—

A category is concrete if it comes equipped with a faithful functor into 

module _ {o β„“} (C : Precategory o β„“) where
  open Cat.Reasoning C

  record Concrete (ΞΊ : Level) : Type (o βŠ” β„“ βŠ” lsuc ΞΊ) where
    no-eta-equality
    field
      Forget : Functor C (Sets ΞΊ)
      has-faithful : is-faithful Forget

Constructing concrete categoriesπŸ”—

When we construct a category, we typically prove the associativity/unitality conditions β€œby hand”. However, this can be quite tedious for syntactic presentations of categories, as it involves a large amount of induction. However, these presentations are often meant to present some category of structured functions between sets: if the presentation is injective, then we can derive the category laws by simply lifting the good definitional behaviour of functions along the presentation function.

The following record contains the data required to perform this trick.

record make-concrete
  {o β„“ : Level}
  (Ob : Type o) (Hom : Ob β†’ Ob β†’ Type β„“)
  : Typeω
  where
  no-eta-equality
  field
    id : βˆ€ {x} β†’ Hom x x
    _∘_ : βˆ€ {x y z} β†’ Hom y z β†’ Hom x y β†’ Hom x z

    {lvl} : Level
    Fβ‚€ : Ob β†’ Type lvl
    Fβ‚€-is-set : βˆ€ {x} β†’ is-set (Fβ‚€ x)

    F₁ : βˆ€ {x y} β†’ Hom x y β†’ Fβ‚€ x β†’ Fβ‚€ y
    F₁-inj : βˆ€ {x y} {f g : Hom x y} β†’ (βˆ€ a β†’ F₁ f a ≑ F₁ g a) β†’ f ≑ g
    F-id : βˆ€ {x} β†’ (a : Fβ‚€ x) β†’ F₁ id a ≑ a
    F-∘ : βˆ€ {x y z} (f : Hom y z) (g : Hom x y) (a : Fβ‚€ x) β†’ F₁ (f ∘ g) a ≑ F₁ f (F₁ g a)

We can show that our putative hom sets are actually sets by lifting the hlevel proof along the injection.

  abstract
    make-is-set
      : βˆ€ x y β†’ is-set (Hom x y)
    make-is-set x y = injectiveβ†’is-set (F₁-inj βŠ™ happly) (fun-is-hlevel 2 Fβ‚€-is-set)

Likewise, all equations can be lifted as well.

    make-idl
      : βˆ€ {x y} (f : Hom x y)
      β†’ id ∘ f ≑ f
    make-idl f = F₁-inj Ξ» a β†’
      F₁ (id ∘ f) a  β‰‘βŸ¨ F-∘ id f a ⟩
      F₁ id (F₁ f a) β‰‘βŸ¨ F-id (F₁ f a) ⟩
      F₁ f a ∎

    make-idr
      : βˆ€ {x y} (f : Hom x y)
      β†’ f ∘ id ≑ f
    make-idr f = F₁-inj Ξ» a β†’
      F₁ (f ∘ id) a  β‰‘βŸ¨ F-∘ f id a ⟩
      F₁ f (F₁ id a) β‰‘βŸ¨ ap (F₁ f) (F-id a) ⟩
      F₁ f a         ∎

    make-assoc
      : βˆ€ {w x y z} (f : Hom y z) (g : Hom x y) (h : Hom w x)
      β†’ f ∘ (g ∘ h) ≑ (f ∘ g) ∘ h
    make-assoc f g h = F₁-inj Ξ» a β†’
      F₁ (f ∘ (g ∘ h)) a   β‰‘βŸ¨ F-∘ f (g ∘ h) a βˆ™ ap (F₁ f) (F-∘ g h a) ⟩
      F₁ f (F₁ g (F₁ h a)) β‰‘Λ˜βŸ¨ F-∘ (f ∘ g) h a βˆ™ F-∘ f g (F₁ h a) ⟩
      F₁ ((f ∘ g) ∘ h) a   ∎

Used naively, make-concrete would result in unreadable goals. To avoid this, we provide macros that expand out the proofs in make-concrete into a top-level definition implemented via copattern matching.

define-concrete-category
  : βˆ€ {o β„“} {Ob : Type o} {Hom : Ob β†’ Ob β†’ Type β„“}
  β†’ Name β†’ make-concrete Ob Hom β†’ TC ⊀

declare-concrete-category
  : βˆ€ {o β„“} {Ob : Type o} {Hom : Ob β†’ Ob β†’ Type β„“}
  β†’ Name β†’ make-concrete Ob Hom β†’ TC ⊀
The details of the macro are omitted to spare the innocent reader. 
make-concrete-category
  : βˆ€ {o β„“} {Ob : Type o} {Hom : Ob β†’ Ob β†’ Type β„“}
  β†’ Bool β†’ Name β†’ make-concrete Ob Hom β†’ TC Name
make-concrete-category {o} {β„“} {Ob} {Hom} declare? nm mk = do
  `mk ← quoteΟ‰TC mk
  `O ← quoteTC Ob
  `H ← quoteTC Hom

  ty ← quoteTC (Precategory o β„“)
  case declare? of Ξ» where
    true β†’ declare (argN nm) ty
    false β†’ pure tt

  -- Need to use field projections to avoid issues with implicit instantiation.
  define-function nm $
    clause [] [ argN (proj (quote Precategory.Ob)) ] `O ∷
    clause [] [ argN (proj (quote Precategory.Hom)) ] `H ∷
    clause
      []
      [ argN (proj (quote Precategory.Hom-set)) ]
      (def (quote make-is-set) [ argN `mk ]) ∷
    clause
      (implicits `O ["x"])
      (argN (proj (quote Precategory.id)) ∷ implicit-patterns 1)
      (def (quote id) [ argN `mk , argH (var 0 []) ]) ∷
    clause
      (implicits `O ["x", "y", "z"])
      (argN (proj (quote Precategory._∘_)) ∷ implicit-patterns 3)
      (def (quote _∘_) [ argN `mk , argH (var 2 []) , argH (var 1 []) , argH (var 0 []) ]) ∷
    clause
      (implicits `O ["x", "y"])
      (argN (proj (quote Precategory.idr)) ∷ implicit-patterns 2)
      (def (quote make-idr) [ argN `mk ,  argH (var 1 []) , argH (var 0 []) ]) ∷
    clause
      (implicits `O ["x", "y"])
      (argN (proj (quote Precategory.idl)) ∷ implicit-patterns 2)
      (def (quote make-idl) [ argN `mk ,  argH (var 1 []) , argH (var 0 []) ]) ∷
    clause
      (implicits `O ["w", "x", "y", "z"])
      (argN (proj (quote Precategory.assoc)) ∷ implicit-patterns 4)
      (def (quote make-assoc) [ argN `mk , argH (var 3 []) , argH (var 2 []) , argH (var 1 []) , argH (var 0 []) ]) ∷
    []
  pure nm
  where
    open make-concrete

    implicits : Term β†’ List String β†’ Telescope
    implicits ty = map (_, argH ty)

    implicit-patterns : Nat β†’ List (Arg Pattern)
    implicit-patterns 0 = []
    implicit-patterns (suc n) = argH (var n) ∷ implicit-patterns n

    implicit-args : Nat β†’ List (Arg Term)
    implicit-args 0 = []
    implicit-args (suc n) = argH (var n []) ∷ implicit-args n

declare-concrete-category nm mk = do
  make-concrete-category true nm mk
  pure tt

define-concrete-category nm mk = do
  make-concrete-category false nm mk
  pure tt