Objects over a strict initial object are terminal

If C has strict initial objects and X is initial, Mathlib identifies Over X with a point (CategoryTheory.overEquivOfIsInitial). This file records the consequence that every object of Over X is terminal, so any two parallel morphisms in Over X are equal. For schemes, apply it to AlgebraicGeometry.isInitialOfIsEmpty: over an empty base scheme every object of the slice category is terminal.

Main declarations

• CategoryTheory.Over.isTerminalOfIsInitial: every object of Over X is terminal when X is a strict initial object.

noncomputable def CategoryTheory.Over.isTerminalOfIsInitial {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasStrictInitialObjects C] {X : C} (h : Limits.IsInitial X) (A : Over X) : Limits.IsTerminal A

If C has strict initial objects and X is initial, every object of Over X is terminal: its structure morphism is an isomorphism, identifying it with Over.mk (𝟙 X).