proposition: Theorem right_adjoint_iso `(F : C ⟶ D) (G G' : D ⟶ C) : F ⊣ G → F ⊣ G' → G ≈ G'.
proof: Proof. intros. construct. - isomorphism. + apply adj; simpl. apply X; simpl. exact id. + apply adj; simpl. apply X0; simpl. exact id. + simpl. rewrite <- to_adj_nat_l. rewrite <- from_adj_nat_l. rewrite id_left. rewrite to_adj_comp_law. rewrite from_adj_comp_law. reflexivity. + simpl. rewrite <- to_adj_nat_l. rewrite <- from_adj_nat_l. rewrite id_left. rewrite to_adj_comp_law. rewrite from_adj_comp_law. reflexivity. - simpl. rewrite <- to_adj_nat_l. rewrite <- from_adj_nat_l. rewrite id_left. rewrite <- to_adj_nat_l. rewrite <- from_adj_nat_l. rewrite <- to_adj_nat_r. rewrite <- from_adj_nat_r. rewrite id_right. rewrite to_adj_comp_law. rewrite from_adj_comp_law. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets