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. 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.
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.