Definition hfiber_functor (X : HSET) (f : HSET / X) : functor (HSET / X) (HSET / X). Proof. use make_functor. + use tpair. * apply (hfiber_fun _ f). * cbn. intros a b g. { use tpair; simpl. - intros h. exists (pr1 h). intros fx. use tpair. * exact (pr1 g (pr1 (pr2 h fx))). * abstract (etrans; [ apply (!toforallpaths _ _ _ (pr2 g) (pr1 (pr2 h fx)))|]; apply (pr2 (pr2 h fx))). - abstract (now apply funextsec). } + split. - intros x; apply (eq_mor_slicecat HSET); simpl. apply funextsec; intros [y hy]. use total2_paths_f; [ apply idpath |]. apply funextsec; intros w; apply subtypePath; [|apply idpath]. now intros XX; apply setproperty. - intros x y z g h; apply (eq_mor_slicecat HSET); simpl. apply funextsec; intros [w hw]. use total2_paths_f; [ apply idpath |]. apply funextsec; intros w'. apply subtypePath; [|apply idpath]. now intros XX; apply setproperty. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits.