{A B C : Type} {f : A -> B} {g : A -> C} (a : A) : pushl (f a) = pushr (g a) := @cglue A (B+C) (inl o f) (inr o g) a.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.