Definition terminal_is_sheaf : is_sheaf C (Terminal_PreShv : PreShv C). Proof. intros X S f. use unique_exists. - apply (TerminalArrow Terminal_PreShv). - abstract apply (TerminalArrowEq (T := Terminal_PreShv)). - abstract ( intro; apply isaset_nat_trans; apply homset_property ). - abstract ( intros x y; apply (TerminalArrowUnique Terminal_PreShv) ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sheaves.