proposition: Lemma sect_pushout_sym_map {A B C f g} : (@pushout_sym_map A B C f g) o (@pushout_sym_map A C B g f) == idmap.
proof: Proof. srapply @Pushout_ind. - intros; reflexivity. - intros; reflexivity. - intro a. simpl. abstract (rewrite transport_paths_FFlr, Pushout_rec_beta_pglue, ap_V, Pushout_rec_beta_pglue; hott_simpl). Defined.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq