Definition total_adjunction_data : adjunction_data (total_category D1) (total_category D2). Proof. use make_adjunction_data. - exact (total_functor LL). - exact (total_functor RR). - use (nat_trans_comp _ _ _ (total_functor_identity D1)). use (nat_trans_comp _ _ _ _ (total_functor_comp_inv _ _)). use total_nat_trans. + exact η. + exact ηη. - use (nat_trans_comp _ _ _ (total_functor_comp _ _)). use (nat_trans_comp _ _ _ _ (total_functor_identity_inv _)). use total_nat_trans. + exact ε. + exact εε. Defined.
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.Core.Isos. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Adjunctions. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.