Initial and terminal objects in a category.
A category has a terminal object if it has a limit over the empty diagram.
Use has_terminal_of_unique to construct instances.
A category has an initial object if it has a colimit over the empty diagram.
Use has_initial_of_unique to construct instances.
The chosen terminal object, if it exists.
You can use the notation ⊤_ C.
This object is characterized by having a unique morphism from any object.
The chosen initial object, if it exists.
You can use the notation ⊥_ C.
This object is characterized by having a unique morphism to any object.
We can more explicitly show that a category has a terminal object by specifying the object, and showing there is a unique morphism to it from any other object.
Equations
- category_theory.limits.has_terminal_of_unique X = {has_limit := λ (F : category_theory.discrete pempty ⥤ C), {cone := {X := X, π := {app := pempty.rec (λ (n : pempty), ((category_theory.functor.const (category_theory.discrete pempty)).obj X).obj n ⟶ F.obj n), naturality' := _}}, is_limit := {lift := λ (s : category_theory.limits.cone F), inhabited.default (s.X ⟶ X), fac' := _, uniq' := _}}}
We can more explicitly show that a category has an initial object by specifying the object, and showing there is a unique morphism from it to any other object.
Equations
- category_theory.limits.has_initial_of_unique X = {has_colimit := λ (F : category_theory.discrete pempty ⥤ C), {cocone := {X := X, ι := {app := pempty.rec (λ (n : pempty), F.obj n ⟶ ((category_theory.functor.const (category_theory.discrete pempty)).obj X).obj n), naturality' := _}}, is_colimit := {desc := λ (s : category_theory.limits.cocone F), inhabited.default (X ⟶ s.X), fac' := _, uniq' := _}}}
The map from an object to the terminal object.
The map to an object from the initial object.