(c : setcone f) : HProp. Proof. pose (fib y := hexists (fun x : X => f x = y)). apply (fun f => @Trunc_rec _ _ HProp _ f c). refine (Pushout_rec HProp fib (fun _ => Unit_hp) (fun x => _)). pose (contr_inhabited_hprop (fib (f x)) (tr (x; idpath))) as i. apply path_hprop. simpl. simpl in i. apply (equiv_contr_unit). Defined.
Require Import Basics. Require Import Types. Require Import TruncType. Require Import ReflectiveSubuniverse. Require Import Colimits.Pushout Truncations.Core HIT.SetCone.