proposition: Lemma nat_trans_to_dinatural_transformation {f : C ↛ C} {g : C ↛ C} (alpha : nat_trans (f : _ ⟶ _) (g : _ ⟶ _)) : f ⇏ g.
proof: 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.
imports: UniMath.Foundations.Preamble UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.All