proposition: Lemma ap_a_path_object' x y Ha Hb Hf : ap (@a) (@path_object' x y Ha Hb Hf) = Ha.
proof: Proof. destruct x, y; simpl in *. destruct Ha, Hb, Hf; simpl in *. reflexivity. Qed.
imports: Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Strict HoTT.Basics HoTT.Types