Require Import HoTT.Basics Types.Unit.
Require Import Colimits.Pushout.
Require Import Truncations.Core.

Section SetCone.
  Context {A B : HSet} (f : A → B).

  Definition setcone := Trunc 0 (Pushout@{_ _ Set _} f (const_tt A)).

  Global Instance istrunc_setcone : IsHSet setcone := _.

  Definition setcone_point : setcone := tr (push (inr tt)).
End SetCone.