Definition fiber {C:category} {X Y:[C^op,SET]} (p : X --> Y) {c:C} (y : c ⇒ Y) : C^op ⟶ SET. Proof. unshelve refine (makeFunctor_op _ _ _ _). - intro b. exists (∑ fx : (b --> c) × (b ⇒ X), p ⟳ pr2 fx = y ⟲ pr1 fx). abstract (apply isaset_total2; [ apply isaset_dirprod, setproperty; apply homset_property | intros [f x]; apply isasetaprop; apply setproperty ]) using _K_. - simpl; intros b b' g fxe. exists (pr1 (pr1 fxe) ∘ g,, pr2 (pr1 fxe) ⟲ g). abstract (simpl; rewrite nattrans_arrow_mor_assoc, arrow_mor_mor_assoc; apply maponpaths; exact (pr2 fxe)) using _M_. - abstract (intro b; apply funextsec; intro w; induction w as [w e]; induction w as [f x]; simpl; unshelve refine (two_arg_paths_f _ _); [ apply dirprodeq; [ apply id_left | apply arrow_mor_id ] | apply setproperty]) using _R_. - abstract (intros b b' b'' g g''; apply funextsec; intro w; induction w as [w e]; induction w as [f x]; simpl; unshelve refine (total2_paths2_f _ _); [ apply dirprodeq; [ apply pathsinv0, assoc | apply arrow_mor_mor_assoc ] | apply setproperty ]) using _T_. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.