Lemma discrete_topos_to_unit_ff : fully_faithful discrete_topos_to_unit_functor. Proof. intros P Q. use isweq_iso. - intro f. apply make_sheaf_morphism. use make_nat_trans. + intros X x. apply discrete_sheaf_value. + abstract ( intros X Y g; apply discrete_sheaf_morphism_irrelevance ). - abstract ( intro f; apply sheaf_morphism_eq; apply nat_trans_eq_alt; intro X; apply discrete_sheaf_morphism_irrelevance ). - abstract ( intro f; apply isasetunit ). Defined.
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.