proposition: Lemma SingletonArrow_isMonic (B: C) : isMonic ({⋅} B).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.SubobjectClassifier UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.PowerObject UniMath.CategoryTheory.Monics UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Subobjects UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.MonoEpiIso