proposition: Lemma path_precategory_uncurried'_fst `{Funext} C D HO HM HC HI : ap object (@path_precategory_uncurried' _ C D (HO; (HM; (HC, HI)))) = HO.
proof: Proof. destruct C, D; cbn in *. path_induction_hammer. Qed.
imports: Category.Core HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall HoTT.Tactics