Definition base_change_functor {c c' : C} (g : C⟦c,c'⟧) : functor (C / c') (C / c) := (base_change_functor_data g,,is_functor_base_change_functor g). Local Definition eta_data {c c' : C} (g : C⟦c,c'⟧) : nat_trans_data (functor_identity (C / c)) (functor_composite (slicecat_functor g) (base_change_functor g)). Proof. intros x. use tpair; simpl. + use (PullbackArrow _ _ (pr2 x) (identity _)). abstract (rewrite id_left; apply idpath). + abstract (rewrite PullbackArrow_PullbackPr1; apply idpath). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.