proposition: Lemma transport_of_relmonad_η_is_pointwise {C : precategory_data} {D : precategory} (J : functor C D) (F0 G0 : ob C -> ob D) (F1 : ∏ a : ob C, J a --> F0 a) (gamma : F0 = G0 ) (c: ob C) : transportf (fun x : ob C -> ob D => ∏ a, D ⟦J a, x a⟧) gamma F1 c = transportf (fun d: ob D => D ⟦J c, d⟧) (toforallpaths (λ _ : ob C, D) F0 G0 gamma c) (F1 c).
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