Definition to_constant_nat_trans {C₁ C₂ : category} (F : C₁ ⟶ C₂) (y : C₂) (fs : ∏ (x : C₁), F x --> y) (ps : ∏ (x₁ x₂ : C₁) (g : x₁ --> x₂), # F g · fs x₂ = fs x₁) : nat_trans F (constant_functor C₁ C₂ y). Proof. use make_nat_trans. - exact (λ x, fs x). - abstract (intros x₁ x₂ g ; cbn ; rewrite id_right ; rewrite ps ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.