fact: Definition codeglue7_to_O (q01 : Q x0 y1) (u : glue q01 @ (glue q11)^ = r) : codeglue7 (to O _ (q01;u)) = to O (hfiber glue (r @ glue q11)) (q01 ; moveL_pM (glue q11) (glue q01) r u) := to_O_equiv_natural _ _ _.
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations