(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics Types.Unit.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Colimits.Pushout.
Require Import Truncations.Core.

(** * Cones of HSets *)

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.