Complete precategories

Content created by Egbert Rijke, Fernando Chu and Fredrik Bakke.

Created on 2024-08-29.
Last modified on 2024-08-29.

module category-theory.complete-precategories where
Imports 
open import category-theory.cones-precategories
open import category-theory.functors-precategories
open import category-theory.limits-precategories
open import category-theory.precategories
open import category-theory.terminal-objects-precategories

open import foundation.universe-levels

Idea

A complete precategory is a precategory that has all limits for diagrams from a specified universe.

More precisely, we say that a precategory D is (l1 , l2)-complete if for any C : Precategory l1 l2 and any functor F : C → D the type of limits of F is inhabited.

Definition

is-complete-Precategory :
  (l1 l2 : Level) {l3 l4 : Level}
  (D : Precategory l3 l4) →
  UU (lsuc l1 ⊔ lsuc l2 ⊔ l3 ⊔ l4)
is-complete-Precategory l1 l2 D =
  (C : Precategory l1 l2) (F : functor-Precategory C D) →
  limit-Precategory C D F

Recent changes