PreCategory. Proof. refine (@Build_PreCategory Pair (fun s d => morphism s d) identity compose _ _ _ _); [ abstract ( intros ? ? ? ? [f ?] [g ?] [h ?]; exact (pseudofunctor_to_cat_assoc_helper (apD10 (ap components_of (p_composition_of_coherent_for_rewrite F _ _ _ _ f g h)))) ) | abstract ( intros ? ? [f ?]; exact (pseudofunctor_to_cat_left_identity_helper (apD10 (ap components_of (p_left_identity_of_coherent_for_rewrite F _ _ f)))) ) | abstract ( intros ? ? [f ?]; exact (pseudofunctor_to_cat_right_identity_helper (apD10 (ap components_of (p_right_identity_of_coherent_for_rewrite F _ _ f)))) ) ]. Defined.
Require Import FunctorCategory.Morphisms. Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Pseudofunctor.Core Pseudofunctor.RewriteLaws. Require Import Category.Morphisms Cat.Morphisms. Require Import Functor.Composition.Core. Require Import Functor.Identity. Require Import FunctorCategory.Core. Require Import Basics Types HoTT.Tactics.