proposition: Lemma path_precategory_uncurried__identity_helper `{Funext} (C D : PreCategory) (Heq : path_precategory'_T C D) : transport _ Heq.2.1 (transportD (fun obj => obj -> obj -> Type) (fun obj mor => forall x, mor x x) Heq.1 (morphism C) (@identity C)) = @identity D.
proof: Proof. destruct Heq as [? [? ?]]; cbn in *. repeat (intro || apply path_forall). apply identity_unique; cbn in *; auto with morphism. destruct C, D; cbn in *. path_induction; cbn in *. auto. 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