{x0 : X} {y : Y} (r : left x0 = right y) : Type := O (hfiber glue r).
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.