{ q01 : Q x0 y1 & glue q01 @ (glue q11)^ = r }.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.