Timings for SetCone.v

(* -*- mode: coq; mode: visual-line -*- *)

Require Import HoTT.Basics Types.Unit.

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.