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. induction gamma. apply idpath. 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.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core.