Lemma empty_sieve_is_monic : isMonic (C := PreShv C) empty_sieve_nat_trans. Proof. apply is_nat_trans_monic_from_pointwise_monics. intro a. apply (invmap (MonosAreInjective_HSET _)). intro e. induction e. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sieves.