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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.Adjunctions.Core.