Definition get_diagram (A C : category) (g : graph) (D : diagram g [A, C]^op) : diagram g [A^op, C^op]. Proof. apply (tpair _ (λ u, from_opp_to_opp_opp _ _ _ (pr1 D u))). intros u v e; simpl. use tpair; simpl. + apply (pr2 D _ _ e). + abstract (intros a b f; apply pathsinv0, (pr2 (pr2 D u v e) b a f)). 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.