Lemma discrete_sheaf_value_unique (x : FX) : x = discrete_sheaf_value. Proof. pose (E := pr2 H (invmap (yoneda_weq C X F) x ,, InitialArrowUnique Initial_PreShv _ _)). refine (!eqtohomot (functor_id F X) x @ _). exact (eqtohomot (nat_trans_eq_weq (homset_property _) _ _ (base_paths _ _ E) X) (identity X)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Presheaf. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.GrothendieckToposes.Examples.EmptySieve. Require Import UniMath.CategoryTheory.GrothendieckToposes.Examples.TerminalSheaf. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sheaves. Require Import UniMath.CategoryTheory.GrothendieckToposes.Sites. Require Import UniMath.CategoryTheory.GrothendieckToposes.Topologies.