Definition has_homsets_shSet_precategory : has_homsets shSet_precategory. Proof. intros F G. simpl. use isaset_set_sfun_space. 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.