Lemma is_functor_base_change_functor {c c' : C} (g : C⟦c,c'⟧) : is_functor (base_change_functor_data g). Proof. split. - intros x; apply (eq_mor_slicecat C); simpl. apply pathsinv0, PullbackArrowUnique; rewrite id_left, ?id_right; apply idpath. - intros x y z f1 f2; apply (eq_mor_slicecat C); simpl. apply pathsinv0, PullbackArrowUnique. + rewrite <- assoc, !PullbackArrow_PullbackPr1; apply idpath. + rewrite <- assoc, PullbackArrow_PullbackPr2, !assoc, PullbackArrow_PullbackPr2; apply idpath. Qed.
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.