proposition: Lemma path_functor_uncurried_idpath F : @path_functor_uncurried F F (idpath; idpath) = idpath.
proof: Proof. destruct F; simpl in *. rewrite !(contr idpath). reflexivity. Qed.
imports: Category.Core Functor.Core HoTT.Basics HoTT.Types HoTT.Tactics