Definition algebra_ob_eq (X Y : FunctorAlg F) : (X = Y) ≃ algebra_eq_type X Y. Proof. eapply weqcomp. - apply total2_paths_equiv. - set (H1 := make_weq _ (H (pr1 X) (pr1 Y))). apply (weqbandf H1). simpl. intro p. destruct X as [X α]. destruct Y as [Y β]; simpl in *. destruct p. rewrite idpath_transportf. unfold is_algebra_mor; simpl. rewrite functor_id. rewrite id_left, id_right. apply idweq. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Coproducts.