Definition ψ_target : functor C^op HSET := functor_composite (functor_opp F) ψ_source. Section general_case. Context (ψ : ψ_source ⟹ ψ_target). Let LchnF : chain D := mapchain L chnF. Let z : D⟦L0,X⟧ := InitialArrow ILD X. Local Definition Pow_source : functor C^op HSET := ψ_source. Local Definition Pow_target (n : nat) : functor C^op HSET := functor_composite (functor_opp (iter_functor F n)) ψ_source. Local Definition Pow (n : nat) : Pow_source ⟹ Pow_target n. Proof. induction n as [|n Pown]. - apply nat_trans_id. - apply (nat_trans_comp Pown (pre_whisker (functor_opp (iter_functor F n)) ψ)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Chains.Chains. Require Import UniMath.CategoryTheory.Chains.Adamek. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.whiskering.