proposition: Lemma is_expDd0_adjunction_laws : form_adjunction' is_expDd0_adjunction_data.
proof: Proof. split. - intro d. change (# Fd0 (ηDd0 d) · εDd0 (Fd0 d) = identity (Fd0 d)). unfold ηDd0. etrans. { apply cancel_postcomposition. etrans. { apply functor_comp. } do 2 apply maponpaths. assert (Hpost := post_whisker_composition _ _ _ F _ _ _ (pre_whisker G (ηC (G d0))) (post_whisker (pr1 μ) (GC (G d0)))). refine (toforallpaths _ _ _ (maponpaths pr1 Hpost) d). } etrans. { apply cancel_postcomposition. apply maponpaths. apply functor_comp. } unfold εDd0. Abort. End FixAnObject. End ExponentialsCarriedThroughAdjointEquivalence. Section AlternativeWithUnivalence. Context {C : category} (PC : BinProducts C) {D : category} (PD : BinProducts D) (ExpC : Exponentials PC) (adjeq : adj_equiv C D) (Cuniv : is_univalent C) (Duniv : is_univalent D). Local Lemma CDeq : C = D. Proof. assert (aux : category_to_precategory C = category_to_precategory D). { apply (invmap (catiso_is_path_precat C D D)). apply (adj_equivalence_of_cats_to_cat_iso adjeq); assumption. } apply subtypePath. intro. apply isaprop_has_homsets. exact aux. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality UniMath.CategoryTheory.Core.Univalence