Lemma nat_trans_to_dinatural_transformation {f : C ↛ C} {g : C ↛ C} (alpha : nat_trans (f : _ ⟶ _) (g : _ ⟶ _)) : f ⇏ g. Proof. use make_dinatural_transformation. - exact (λ z, alpha (_ ,, _)). - abstract (intros a b h ; use funextsec ; intro z ; unfold lmap, rmap ; pose (p := eqtohomot (nat_trans_ax alpha (_ ,, _) (_ ,, _) (h ,, identity _)) z) ; cbn in p ; cbn ; refine (maponpaths _ p @ _) ; clear p ; refine (!(profunctor_comp g _ _ _ _ _) @ _) ; rewrite !id_left ; refine (!_) ; refine (maponpaths _ (eqtohomot (nat_trans_ax alpha (_ ,, _) (_ ,, _) (_ ,, _)) _) @ _) ; refine (!(profunctor_comp g _ _ _ _ _) @ _) ; rewrite !id_right ; apply idpath). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.All.