proposition: Theorem Functor_Setoid_Nat_Iso `(F : C ⟶ D) (G : C ⟶ D) : F ≅[Fun] G ↔ F ≈ G.
proof: Proof. split; intros; simpl. - given (iso : ∀ x : C, F x ≅ G x). { intros; isomorphism; simpl; intros. - apply X. - apply (X⁻¹). - abstract (srewrite (iso_to_from X); cat). - abstract (srewrite (iso_from_to X); cat). } exists iso; simpl in *; intros. abstract (rewrite <- comp_assoc; rewrite (naturality[to X]); rewrite comp_assoc; srewrite (iso_from_to X); cat). - destruct X. isomorphism; simpl; intros. + transform; simpl; intros. * apply x. * abstract (rewrite e; simpl; rewrite !comp_assoc; rewrite iso_to_from; cat). * abstract (rewrite e; simpl; rewrite !comp_assoc; rewrite iso_to_from; cat). + transform; simpl; intros. * apply x. * abstract (rewrite e; simpl; rewrite <- !comp_assoc; rewrite iso_to_from; cat). * abstract (rewrite e; simpl; rewrite <- !comp_assoc; rewrite iso_to_from; cat). + abstract (rewrite fmap_id; apply iso_to_from). + abstract (rewrite fmap_id; apply iso_from_to). Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Instance.Sets