(u : V) : V@{U' U} := set (Unit_ind u). Global Instance isequiv_ap_V_singleton {u v : V} : IsEquiv (@ap _ _ u v). Proof. simple refine (Build_IsEquiv _ _ _ _ _ _ _); try solve [ intro; apply path_ishprop ]. { intro H. specialize (path_V_eqimg H). intros (H1, H2). refine (Trunc_rec _ (H1 tt)). intros [t p]. destruct t; exact p. } Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Colimits.SpanPushout. Require Import HoTT.Truncations.Core Colimits.Quotient.