Discrete categories
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-05-06.
Last modified on 2023-06-25.
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.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 pr1 discrete-precategory-Set = type-Set X pr1 (pr2 discrete-precategory-Set) x y = set-Prop (x = y , is-set-type-Set X x y) pr1 (pr1 (pr2 (pr2 discrete-precategory-Set))) = concat' _ pr2 (pr1 (pr2 (pr2 discrete-precategory-Set))) refl refl refl = refl pr1 (pr2 (pr2 (pr2 discrete-precategory-Set))) x = refl pr1 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = right-unit pr2 (pr2 (pr2 (pr2 (pr2 discrete-precategory-Set)))) _ = left-unit
Recent changes
- 2023-06-25. Fredrik Bakke. Fix alignment
where
blocks (#670). - 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).