Definition get_cocone (A C : category) (g : graph) (D : diagram g [A, C]^op) (F : functor A C) (ccF : cocone D F) : cocone (get_diagram A C g D) (functor_opp F). Proof. destruct ccF as [t p]. use make_cocone. - intro u; apply (tpair _ (pr1 (t u))). abstract (intros a b f; apply pathsinv0, (pr2 (t u) b a f)). - abstract (intros u v e; apply (nat_trans_eq C^op ); now intro a; simpl; rewrite <- (p u v e)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.