Discrete categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-05-06.
Last modified on 2024-03-11.

module category-theory.discrete-categories where
Imports 
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.strictly-involutive-identity-types
open import foundation.universe-levels

Discrete precategories

Any set induces a discrete category whose objects are elements of the set and which contains no-nonidentity morphisms.

module _
  {l : Level} (X : Set l)
  where

  discrete-precategory-Set : Precategory l l
  discrete-precategory-Set =
    make-Precategory
      ( type-Set X)
      ( λ x y → set-Prop (Id-Prop X x y))
      ( λ p q → q ∙ p)
      ( λ x → refl)
      ( λ h g f → inv (assoc f g h))
      ( λ _ → right-unit)
      ( λ _ → left-unit)

Recent changes