Definition is_univalent_structure_unit_binop : is_univalent unit_binop_structure_cat. Proof. use is_univalent_total_category. - apply binop. - apply is_univalent_disp_from_fibers. intros x xx yy. use isweqimplimpl. + intros f. use subtypePath. { intro ; apply isapropdirprod ; use impred ; intro ; apply setproperty. } exact (pr11 f). + apply isapropifcontr. apply isaprop_has_unit. + use invproofirrelevance. intros f g. use subtypePath. { intro ; apply isaprop_is_z_iso_disp. } use subtypePath. { intro ; apply isapropunit. } apply setproperty. 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.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma.