open import Cat.Instances.Shape.Interval
open import Cat.Instances.Discrete
open import Cat.Prelude

open import Data.Fin.Finite

open Precategory
module Cat.Finite where

Finite precategoriesπŸ”—

A precategory is finite if both its type of objects and its total space of morphisms are finite.

record is-finite-precategory {o β„“} (D : Precategory o β„“) : Type (o βŠ” β„“) where
  constructor finite-cat
  field
    ⦃ has-finite-Ob ⦄ : Finite (Ob D)
    ⦃ has-finite-Arrows ⦄ : Finite (Arrows D)

open is-finite-precategory
_ = Finite-Ξ£
_ = Finite-PathP

Conveniently, because finite types are closed under Ξ£, it suffices that each Hom set be finite:

finite-cat-hom
  : βˆ€ {o β„“} {D : Precategory o β„“}
  β†’ ⦃ Finite (Ob D) ⦄
  β†’ (βˆ€ a b β†’ Finite (Hom D a b))
  β†’ is-finite-precategory D
finite-cat-hom {D = D} f = finite-cat where
  instance
    finite-Hom : βˆ€ {a b} β†’ Finite (Hom D a b)
    finite-Hom {a} {b} = f a b

Thanks to even more instance magic (path types of a finite type are finite), the discrete category on a finite set is finite:

Disc-finite : βˆ€ {β„“} {A : Type β„“} {isg : is-groupoid A} β†’ ⦃ Finite A ⦄
            β†’ is-finite-precategory (Disc A isg)
Disc-finite = finite-cat