proposition: Lemma unique_helper2 : transport (fun GO : C -> prod_type A B => forall s d : C, morphism C s d -> prod_type (morphism A (fst_type (GO s)) (fst_type (GO d))) (morphism B (snd_type (GO s)) (snd_type (GO d)))) (path_forall (a * b) F unique_helper) (fun (s d : C) (m : morphism C s d) => pair_type (a _1 m) (b _1 m)) = morphism_of F.
proof: Proof. repeat (apply path_forall; intro). repeat match goal with | _ => reflexivity | _ => progress simpl | _ => rewrite !transport_forall_constant end. transport_path_forall_hammer. unfold unique_helper. repeat match goal with | [ H : _ = _ |- _ ] => case H; simpl; clear H end. repeat match goal with | [ |- context[@morphism_of ?C ?D ?F ?s ?d ?m] ] => destruct (@morphism_of C D F s d m); clear m | [ |- context[@object_of ?C ?D ?F ?x] ] => destruct (@object_of C D F x); clear x end. reflexivity. Qed.
imports: Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core Functor.Paths Types.Prod HoTT.Tactics Types.Forall Types.Sigma Basics.Tactics