Definition is_univalent_bincoprod_of_category {C₁ C₂ : category} (HC₁ : is_univalent C₁) (HC₂ : is_univalent C₂) : is_univalent (bincoprod_of_category C₁ C₂). Proof. intros z₁ z₂. induction z₁ as [ x₁ | y₁ ] ; induction z₂ as [ x₂ | y₂ ] ; cbn. - use weqhomot. + exact (inl_iso x₁ x₂ ∘ make_weq _ (HC₁ x₁ x₂) ∘ paths_inl_inl_equiv x₁ x₂)%weq. + abstract (intro p ; use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ; cbn -[equality_by_case] ; refine (@idtoiso_in_bincoprod_inl C₁ C₂ _ _ (paths_inl_inl_equiv _ _ _) @ _) ; do 2 apply maponpaths ; apply (homotinvweqweq (paths_inl_inl_equiv _ _))). - use isweq_iso. + exact (λ f, fromempty (pr1 f)). + intro p ; cbn. exact (fromempty (negpathsii1ii2 _ _ p)). + intro p ; cbn. exact (fromempty (pr1 p)). - use isweq_iso. + exact (λ f, fromempty (pr1 f)). + intro p ; cbn. exact (fromempty (negpathsii2ii1 _ _ p)). + intro p ; cbn. exact (fromempty (pr1 p)). - use weqhomot. + exact (inr_iso y₁ y₂ ∘ make_weq _ (HC₂ y₁ y₂) ∘ paths_inr_inr_equiv y₁ y₂)%weq. + abstract (intro p ; use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ; cbn -[equality_by_case] ; refine (@idtoiso_in_bincoprod_inr C₁ C₂ _ _ (paths_inr_inr_equiv _ _ _) @ _) ; do 2 apply maponpaths ; apply (homotinvweqweq (paths_inr_inr_equiv _ _))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering.