(A B : pType) : (@pconst A B) = zero_morphism := idpath. Global Instance is1cat_pforall (A : pType) (P : pFam A) : Is1Cat (pForall A P) | 10. Proof. snrapply Build_Is1Cat'. 1, 2: exact _. - intros f g h p; rapply Build_Is0Functor. intros q r s. exact (phomotopy_postwhisker s p). - intros f g h p; rapply Build_Is0Functor. intros q r s. exact (phomotopy_prewhisker p s). - intros ? ? ? ? p q r. simpl. exact (phomotopy_compose_assoc p q r). - intros ? ? p; exact (phomotopy_compose_p1 p). - intros ? ? p; exact (phomotopy_compose_1p p). Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.