proposition: Lemma path_precategory `{fs : Funext} (C D : PreCategory) : forall (Hobj : object C = object D) (Hmor : forall s d, morphism C (transport idmap Hobj^ s) (transport idmap Hobj^ d) = morphism D s d), (forall s d d' m m', transport idmap (Hmor _ _) (@compose C _ _ _ (transport idmap (Hmor _ _)^ m) (transport idmap (Hmor _ _)^ m')) = @compose D s d d' m m') -> C = D.
proof: Proof. intros Hobj Hmor Hcomp. pose (path_forall _ _ (fun s => path_forall _ _ (fun d => (ap10 (@transport_arrow Type idmap (fun x => x -> Type) _ _ Hobj (@morphism C) _) _) @ (@transport_arrow Type idmap _ _ _ Hobj (@morphism C _) _) @ (transport_const _ _) @ Hmor s d))) as Hmor'. eapply (path_precategory' C D Hobj Hmor'). repeat (apply path_forall; intro). refine (_ @ Hcomp _ _ _ _ _); clear Hcomp. subst Hmor'. cbn. abstract ( destruct C, D; cbn in *; destruct Hobj; cbn in *; repeat match goal with | _ => reflexivity | _ => rewrite !concat_1p | _ => rewrite !transport_forall_constant, !transport_arrow | _ => progress transport_path_forall_hammer | [ |- transport ?P ?p^ ?u = ?v ] => (apply (@moveR_transport_V _ P _ _ p u v); progress transport_path_forall_hammer) | [ |- ?u = transport ?P ?p^ ?v ] => (apply (@moveL_transport_V _ P _ _ p u v); progress transport_path_forall_hammer) | [ |- context[?H ?x ?y] ] => (destruct (H x y); clear H) | _ => progress f_ap end ). Defined.
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