codeleft <~> coderight (r @ glue q11) := codeglue7 oE codeglue6 oE codeglue5 oE codeglue4 oE codeglue3 oE codeglue2 oE codeglue1.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.