proposition: Lemma transport_of_relmonad_bind_is_pointwise {C : precategory_data} {D : precategory} (J : functor C D) (F0 G0 : ob C -> ob D) (F1 : ∏ a b : ob C , D ⟦J a, F0 b⟧ → D ⟦F0 a, F0 b⟧) (gamma : F0 = G0 ) (c d : ob C) (f : J c --> G0 d) : transportf (fun x : ob C -> ob D => ∏ a b : ob C , D ⟦J a, x b⟧ → D ⟦x a, x b⟧) gamma F1 c d f = double_transport (toforallpaths (λ _ : ob C, D) F0 G0 gamma c) (toforallpaths (λ _ : ob C, D) F0 G0 gamma d) (F1 c d (transportb (fun x : ob D => D ⟦J c, x⟧) (toforallpaths (λ _ : ob C, D) F0 G0 gamma d) f)).
proof: Proof. induction gamma. apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core