proposition: Lemma dagger_functor_cat_is_dagger_univalent {C D : category} (dagC : dagger C) (dagD : dagger D) (u : is_univalent_dagger dagD) : is_univalent_dagger (dagger_on_functor_cat dagC dagD).
proof: Proof. intros F G. use weqhomot. - exact (univalence_iso (pr2 F) (pr2 G) u). - intro p. induction p. use subtypePath. { intro ; apply isaprop_is_unitary. } use subtypePath. { intro ; apply isapropunit. } apply (nat_trans_eq (pr2 D)). intro ; 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