proposition: 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: Proof. induction gamma. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DaggerCategories.Categories UniMath.CategoryTheory.DaggerCategories.Unitary UniMath.CategoryTheory.DaggerCategories.Univalence UniMath.CategoryTheory.DaggerCategories.Functors UniMath.CategoryTheory.DaggerCategories.Transformations