Subterminal precategories
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2024-01-27.
module category-theory.subterminal-precategories where
Imports
open import category-theory.composition-operations-on-binary-families-of-sets open import category-theory.fully-faithful-functors-precategories open import category-theory.isomorphisms-in-precategories open import category-theory.precategories open import category-theory.pregroupoids open import category-theory.preunivalent-categories open import category-theory.strict-categories open import category-theory.terminal-category open import foundation.action-on-identifications-functions open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.equivalences open import foundation.function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.identity-types open import foundation.iterated-dependent-product-types open import foundation.propositions open import foundation.sets open import foundation.subtype-identity-principle open import foundation.unit-type open import foundation.universe-levels
Idea
A precategory is subterminal if its terminal projection functor is fully faithful.
Definitions
The predicate on precategories of being subterminal
module _ {l1 l2 : Level} (C : Precategory l1 l2) where is-subterminal-Precategory : UU (l1 ⊔ l2) is-subterminal-Precategory = is-fully-faithful-functor-Precategory C terminal-Precategory ( terminal-functor-Precategory C) is-subterminal-prop-Precategory : Prop (l1 ⊔ l2) is-subterminal-prop-Precategory = is-fully-faithful-prop-functor-Precategory C terminal-Precategory ( terminal-functor-Precategory C) is-prop-is-subterminal-Precategory : is-prop is-subterminal-Precategory is-prop-is-subterminal-Precategory = is-prop-is-fully-faithful-functor-Precategory C terminal-Precategory ( terminal-functor-Precategory C)
Recent changes
- 2024-01-27. Egbert Rijke. Fix "The predicate of" section headers (#1010).
- 2023-11-24. Fredrik Bakke. Subterminal precategories and constant functors (#941).