proposition: Lemma weq_ob (c : C) : ∃! x : (∑ x : C, D x), pr1 x = c.
proof: Proof. use tpair. - simple refine ((c ,, _) ,, _). + apply uo. + apply idpath. - intros [[c' d'] p]. cbn in *. use total2_paths_f. + use subtypePath. { intro ; apply isapropifcontr, uo. } exact p. + simpl. etrans. { apply (transportf_total2_paths_f (A := C) (B := λ x : C, D x) (λ x : C, x = c)). } induction p. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.catiso UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence