{-# OPTIONS --without-K --safe #-}
module Categories.Category.Discrete where

-- Discrete Category.
-- https://ncatlab.org/nlab/show/discrete+category
-- says:
-- A category is discrete if it is both a groupoid and a preorder. That is,
-- every morphism should be invertible, any two parallel morphisms should be equal.
-- The idea is that in a discrete category, no two distinct (nonisomorphic) objects
-- are connectable by any path (morphism), and an object connects to itself only through
-- its identity morphism.

open import Level using (Level; suc; _⊔_)

open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (IsGroupoid)

record IsDiscrete {o  e} (C : Category o  e) : Set (o    e) where
  open Category C using (Obj; _⇒_; _≈_)
  field
     isGroupoid : IsGroupoid C
     preorder : {A B : Obj}  (f g : A  B)  f  g

record DiscreteCategory (o  e : Level) : Set (suc (o    e)) where
  field
    category   : Category o  e
    isDiscrete : IsDiscrete category

  open IsDiscrete isDiscrete public