Proposition triangle_1_over_id_alt {C : category} {D₁ : disp_cat C} {D₂ : disp_cat C} (LL : disp_functor (functor_identity _) D₁ D₂) (HLL : is_equiv_over_id LL) {x : C} (xx : D₁ x) : ♯ LL (inv_mor_disp_from_z_iso (is_z_iso_unit_over_id HLL x xx)) = counit_over_id HLL x (LL x xx). Proof. refine (_ @ !(id_left_disp_var _)). rewrite disp_functor_id_var. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. refine (!_). etrans. { apply maponpaths. apply maponpaths_2. apply maponpaths. exact (!(transportf_transpose_left (z_iso_disp_after_inv_mor (is_z_iso_unit_over_id HLL x xx)))). } rewrite disp_functor_transportf. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. rewrite disp_functor_comp. unfold transportb. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. rewrite assoc_disp_var. rewrite transport_f_f. etrans. { do 2 apply maponpaths. exact (triangle_1_over_id HLL x xx). } unfold transportb. rewrite mor_disp_transportf_prewhisker. rewrite transport_f_f. rewrite id_right_disp. unfold transportb. rewrite transport_f_f. apply transportf_set. apply homset_property. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. 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.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.