Definition bifinal_one_types : is_bifinal unit_one_type. Proof. use make_is_bifinal. - exact (λ _ _, tt). - exact (λ _ _ _ _, pr1 (isapropunit _ _)). - intros Y f g α β. cbn in *. apply funextsec ; intro z. unfold homotsec in α,β. apply isasetunit. Defined.
Require Import UniMath.Foundations.All. 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.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers.