Initial objects of a precategory
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-21.
Last modified on 2023-09-21.
module category-theory.initial-objects-precategories where
Imports
open import category-theory.precategories open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.propositions open import foundation.universe-levels open import foundation-core.identity-types
Idea
The initial object of a precategory (if it exists) is an object with the universal property that there is a unique morphism from it to any object.
Definition
The universal property of initial objects in precategories
module _ {l1 l2 : Level} (C : Precategory l1 l2) (X : obj-Precategory C) where is-initial-prop-obj-Precategory : Prop (l1 ⊔ l2) is-initial-prop-obj-Precategory = Π-Prop ( obj-Precategory C) ( λ Y → is-contr-Prop (type-hom-Precategory C X Y)) is-initial-obj-Precategory : UU (l1 ⊔ l2) is-initial-obj-Precategory = type-Prop is-initial-prop-obj-Precategory is-prop-is-initial-obj-Precategory : is-prop is-initial-obj-Precategory is-prop-is-initial-obj-Precategory = is-prop-type-Prop is-initial-prop-obj-Precategory
The type of initial objects in a precategory
initial-object-Precategory : {l1 l2 : Level} (C : Precategory l1 l2) → UU (l1 ⊔ l2) initial-object-Precategory C = Σ (obj-Precategory C) λ i → (x : obj-Precategory C) → is-contr (type-hom-Precategory C i x) module _ {l1 l2 : Level} (C : Precategory l1 l2) (i : initial-object-Precategory C) where object-initial-object-Precategory : obj-Precategory C object-initial-object-Precategory = pr1 i morphism-initial-object-Precategory : (x : obj-Precategory C) → type-hom-Precategory C object-initial-object-Precategory x morphism-initial-object-Precategory x = pr1 (pr2 i x) is-unique-morphism-initial-object-Precategory : (x : obj-Precategory C) (f : type-hom-Precategory C object-initial-object-Precategory x) → morphism-initial-object-Precategory x = f is-unique-morphism-initial-object-Precategory x = pr2 (pr2 i x)
Recent changes
- 2023-09-21. Egbert Rijke. The classification of cyclic rings (#757).
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).