Lemma transport_of_dagger_functor_map_is_pointwise (F0 G0 : pr11 C -> pr11 D) (F1 : ∏ a b : pr11 C, a --> b -> F0 a --> F0 b) (gamma : F0 = G0 ) (a b : pr11 C) (f : a --> b) : transportf (fun x : pr11 C -> pr11 D => ∏ a0 b0 : pr11 C, a0 --> b0 -> x a0 --> x b0) gamma F1 a b f = Univalence.double_transport (toforallpaths (λ _ : pr11 C, pr11 D) F0 G0 gamma a) (toforallpaths (λ _ : pr11 C, pr11 D) F0 G0 gamma b) (F1 a b f). Proof. induction gamma. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence. Require Import UniMath.CategoryTheory.DaggerCategories.Functors. Require Import UniMath.CategoryTheory.DaggerCategories.Transformations.