Definition p1types_disp_prebicat_ops : disp_prebicat_ops p1types_disp_prebicat_1_id_comp_cells. Proof. repeat split; cbn. - intros X Y f x y ff. exact (pathscomp0rid _ @ maponpathsidfun _). - intros X Y f x y ff. exact (!(pathscomp0rid _ @ maponpathsidfun _)). - intros X Y Z W f g h x y z w ff gg hh. refine (_ @ !(path_assoc _ _ _)). refine (maponpaths (λ z, z @ hh) _). refine (maponpathscomp0 h (maponpaths g ff) gg @ _). refine (maponpaths (λ z, z @ _) _). apply maponpathscomp. - intros X Y Z W f g h x y z w ff gg hh. refine (!_). refine (_ @ !(path_assoc _ _ _)). refine (maponpaths (λ z, z @ hh) _). refine (maponpathscomp0 h (maponpaths g ff) gg @ _). refine (maponpaths (λ z, z @ _) _). apply maponpathscomp. - intros X Y f g h α β x y ff gg hh αα ββ. exact (αα @ maponpaths (λ z, _ @ z) ββ @ path_assoc _ _ _). - intros X Y Z f g h α x y z ff gg hh αα. unfold funhomotsec. refine (maponpaths (λ z, _ @ z) αα @ _). refine (path_assoc _ _ _ @ _ @ !(path_assoc _ _ _)). refine (maponpaths (λ z, z @ _) _). apply homotsec_natural. - intros X Y Z f g h α x y z ff gg hh αα. unfold homotfun. refine (_ @ !(path_assoc _ _ _)). refine (maponpaths (λ z, z @ hh) _). exact (maponpaths (maponpaths h) αα @ maponpathscomp0 h (α x) gg). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.OneTypes. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.