proposition: Lemma is_nat_trans_ψ_from_comps : is_nat_trans ψ_source ψ_target (λ (A : C^op) (f : yoneda_objects_ob C' X (L A)), θ A· # G f· ρ).
proof: Proof. intros A B h. apply funextfun. intro f. simpl. unfold compose at 1 5; simpl. rewrite functor_comp. repeat rewrite assoc. assert (θ_nat_trans_ax := nat_trans_ax θ). unfold functor_composite in θ_nat_trans_ax. simpl in θ_nat_trans_ax. rewrite <- θ_nat_trans_ax. apply idpath. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Adjunctions.Core