Lemma isinitial_termalgebra : Initial (category_algebras). Proof. exists (term_hSetalgebra σ). intro a. apply (iscontrhomsfromgterm (hSetalgebra_to_algebra a)). apply (has_supportsets_hSetalgebra a). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.Algebra.Universal.TermAlgebras.