Lemma slice_fam_form_adj : form_adjunction fam_to_slice slice_to_fam fam_unit slice_counit. Proof. unfold form_adjunction. split. + intro f. apply eq_mor_slicecat. apply funextsec. intro x. reflexivity. + intro F. apply (nat_trans_eq has_homsets_HSET). intro x. apply funextsec. intro f. apply (invmaponpathsincl pr1). - apply isofhlevelfpr1. intro. apply setproperty. - simpl. unfold hfiber. rewrite transportf_total2. simpl. rewrite transportf_const. reflexivity. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Slice. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Categories.StandardCategories.