Lemma weq_ob (c : C) : ∃! x : (∑ x : C, D x), pr1 x = c. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.