Lemma uf0 {c1 c2 : C} (f : C⟦c1,c2⟧) : ∏ (d1 : D c1) (d2 : D c2), iscontr (d1 -->[f] d2). Proof. intros d1 d2. use (iscontrweqb' (is_contr_disp_mor _ _ f)). apply uf_eq. Defined.
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.