proposition: Lemma path_functor_uncurried_fst F G HO HM : ap object_of (@path_functor_uncurried F G (HO; HM)) = HO.
proof: Proof. destruct F, G; simpl in *. path_induction_hammer. Qed.
imports: Category.Core Functor.Core HoTT.Basics HoTT.Types HoTT.Tactics