Proposition is_univalent_collage_profunctor_category (H₁ : is_univalent C₁) (H₂ : is_univalent C₂) : is_univalent collage_profunctor_category. Proof. intros x₁ x₂. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ]. - use weqhomot. + exact (make_weq _ (H₁ _ _) ∘ paths_inl_inl_equiv _ _)%weq. + intro p ; cbn -[equality_by_case_equiv]. use z_iso_eq. refine (idtoiso_in_collage_inl (paths_inl_inl_equiv x₁ x₂ p) @ _). do 2 apply maponpaths. apply (homotinvweqweq (paths_inl_inl_equiv _ _)). - use weqhomot. + refine (invweq _ ∘ paths_inl_inr_equiv _ _)%weq. use weqtoempty. intro f. exact (pr1 f). + intro p. use fromempty. exact (negpathsii1ii2 _ _ p). - use weqhomot. + refine (invweq _ ∘ paths_inr_inl_equiv _ _)%weq. use weqtoempty. intro f. exact (inv_from_z_iso f). + intro p. use fromempty. exact (negpathsii2ii1 _ _ p). - use weqhomot. + exact (make_weq _ (H₂ _ _) ∘ paths_inr_inr_equiv _ _)%weq. + intro p ; cbn -[equality_by_case_equiv]. use z_iso_eq. refine (idtoiso_in_collage_inr (paths_inr_inr_equiv y₁ y₂ p) @ _). do 2 apply maponpaths. apply (homotinvweqweq (paths_inr_inr_equiv _ _)). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares.