proposition: Theorem Adjunction_Comma `{F : D ⟶ C} `{G : C ⟶ D} : F ⊣ G ↔ @lawvere_equiv _ _ F G.
proof: Proof. split; intros H. { unshelve refine {| lawvere_iso := Comma_F_Id_Id_G_Iso H |}. - unshelve eexists; intros; split; destruct f; simpl; cat. - unshelve eexists; intros; split; destruct f; simpl; cat. - unfold whisker_equiv. split; intros; simpl; intros; cat. } apply Adjunction_from_Transform. exact (Build_Adjunction_Transform (@lawvere_eqv_unit_transform _ _ _ _ H) (@lawvere_eqv_counit_transform _ _ _ _ H) (@lawvere_eqv_counit_fmap_unit _ _ _ _ H) (@lawvere_eqv_fmap_counit_unit _ _ _ _ H)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Adjunction Category.Adjunction.Natural.Transformation Category.Adjunction.Natural.Transformation.Universal Category.Construction.Comma Category.Construction.Product Category.Instance.Cat Category.Instance.Fun Category.Instance.Sets