Lemma SingletonArrow_isMonic (B: C) : isMonic ({⋅} B). Proof. use make_isMonic. intros X b b' p. assert (q : (((identity B) ⨱ b) · (δ B) = ((identity B) ⨱ b') · (δ B))). { rewrite (PowerObject_transpose_tri P (δ B)). fold BinProd. rewrite !assoc, !BinProductOfArrows_idxcomp. use (maponpaths (( nat_z_iso_inv (PowerObject_nat_z_iso P)) (X,,B))). exact p. } set (pbr := subobject_classifier_pullback Ω (diagonalMap BinProd B)). set (pbl := auxpb b). set (pbl' := auxpb b'). set (pb := pullback_glue_pullback C pbr pbl). set (pb' := pullback_glue_pullback C pbr pbl'). fold δ B in pb, pb'. transparent assert (pb'' : (Pullback ((identity B) ⨱ b' · δ B) Ω)). { use (Pullback_mor_paths q (idpath _)). exact pb. } induction (pullbackiso _ pb' pb'') as (h,(h_tri1,h_tri2)). cbn - [BinProd] in h, h_tri1. rewrite (precompWithBinProductArrow _ (BinProd B X)) in h_tri1. assert (h_tri11 := (maponpaths (λ f, compose f (BinProductPr1 C (BinProd B X))) h_tri1)). cbn beta in h_tri11. rewrite !BinProductPr1Commutes in h_tri11. assert (h_tri12 := (maponpaths (λ f, compose f (BinProductPr2 C (BinProd B X))) h_tri1)). cbn beta in h_tri12. rewrite !BinProductPr2Commutes, id_right in h_tri12. rewrite h_tri12, id_left in h_tri11. exact h_tri11. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.PowerObject. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Subobjects. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. (PowerObject (BinProductsFromPullbacks PB T) Ω). (Ω: subobject_classifier T) (P: PowerObject (BinProductsFromPullbacks PB T) Ω) Definition Topos_BinProducts : BinProducts Topos_category := BinProductsFromPullbacks (Topos_Pullbacks) (Topos_Terminal).