proposition: Lemma σ_from_τ_is_conjugate {C C' D D' : category} {L : functor D C} {R : functor C D} {L' : functor D' C'} {R' : functor C' D'} {H : functor C C'} {K : functor D D' } (h : are_adjoints L R) (h' : are_adjoints L' R') (hs : has_homsets C') (τ : DistrLaw K H R R') : are_conjugates' h h' (σ_from_τ h h' τ) τ.
proof: Proof. red. intros A B g. unfold σ_from_τ. simpl. unfold σ_data_from_τ. set (η := (unit_from_are_adjoints h)). etrans. { apply pathsinv0. apply φ_adj_inv_natural_postcomp. } apply maponpaths. set (Hτ := nat_trans_ax τ). etrans. { rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply Hτ. } rewrite assoc. apply cancel_postcomposition. change (# (R ∙ K) (φ_adj_inv h g)) with (# K (# R (φ_adj_inv h g))). etrans. { apply pathsinv0. use functor_comp. } apply maponpaths. change (nat_trans_data_from_nat_trans η A · # R (φ_adj_inv h g)) with (φ_adj h (φ_adj_inv h g)). apply φ_adj_after_φ_adj_inv. Qed.
imports: UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Adjunctions.Core