Proposition right_from_left_beck_chevalley_inverses (xx : D[{x}]) : is_inverse_in_precat (ρ xx) (right_from_left_beck_chevalley_inv xx). Proof. unfold right_from_left_beck_chevalley_inv. split. - rewrite !functor_comp. rewrite !assoc'. etrans. { rewrite !assoc. do 4 apply maponpaths_2. apply (nat_trans_ax φ₁ _ _ (ρ xx)). } cbn. rewrite !assoc'. refine (_ @ pr222 S₁ _). apply maponpaths. rewrite <- !functor_comp. apply maponpaths. cbn. assert ((pr212 S₁) (R₁ xx) = ψ₁ (R₁ xx)) as q. { apply idpath. } refine (_ @ !q) ; clear q. rewrite !assoc. etrans. { apply maponpaths_2. apply (nat_trans_ax η₁ _ _ (#L₁ (ρ xx))). } cbn. rewrite !assoc'. rewrite <- functor_comp. etrans. { do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. apply (nat_trans_ax ℓi _ _ (ρ xx)). } cbn. rewrite !assoc'. etrans. { do 3 apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite <- functor_comp. apply maponpaths. rewrite dual_right_beck_chevalley_nat_trans_ob. rewrite !functor_comp. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- !functor_comp. etrans. { apply maponpaths_2. apply maponpaths. refine (!_). apply (functor_comp R₂). } apply (nat_trans_ax ε₂ _ _). } cbn. rewrite !assoc. do 2 apply maponpaths_2. apply (pr122 P₂). } cbn. rewrite id_left. etrans. { do 3 apply maponpaths. rewrite functor_comp. rewrite !assoc'. apply maponpaths. apply (nat_trans_ax ψ₂). } cbn. etrans. { do 3 apply maponpaths. refine (!_). apply dual_left_beck_chevalley_nat_trans_ob_alt. } etrans. { do 2 apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. exact (z_iso_after_z_iso_inv (nat_z_iso_pointwise_z_iso ℓ_iso (G(R₁ xx)))). } rewrite id_left. rewrite functor_comp. rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply (nat_trans_ax η₁). } cbn. rewrite !assoc'. etrans. { apply maponpaths. apply (pr222 P₁). } apply id_right. - cbn. rewrite !assoc'. etrans. { apply maponpaths. etrans. { apply maponpaths_2. apply functor_comp. } rewrite !assoc'. apply maponpaths. apply (nat_trans_ax ρ). } cbn. rewrite dual_right_beck_chevalley_nat_trans_ob. etrans. { rewrite !assoc. do 3 apply maponpaths_2. apply (nat_trans_ax η₂ _ _ (_ · #G(η₁(L₁(R₂(K xx)))))). } cbn. refine (_ @ pr222 P₂ _). rewrite !assoc'. apply maponpaths. rewrite <- !functor_comp. apply maponpaths. cbn. assert ((pr212 P₂) (K xx) = ε₂(K xx)) as q. { apply idpath. } refine (_ @ !q) ; clear q. etrans. { apply maponpaths_2. apply functor_comp. } rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply (nat_trans_ax τ). } cbn. rewrite !assoc'. etrans. { do 2 apply maponpaths. rewrite <- functor_comp. apply maponpaths. rewrite !assoc. do 3 apply maponpaths_2. apply (pr122 P₁). } rewrite id_left. rewrite !assoc. etrans. { apply maponpaths_2. apply dual_left_beck_chevalley_nat_trans_ob_alt'. } rewrite !assoc'. etrans. { apply maponpaths. refine (!(functor_comp K _ _) @ _). apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. exact (z_iso_inv_after_z_iso (nat_z_iso_pointwise_z_iso ℓ_iso (R₂(K xx)))). } rewrite id_left. rewrite functor_comp. rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply (nat_trans_ax φ₂). } cbn. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. apply (pr222 S₂). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums. Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.