proposition: Lemma ap_iso_from_to (ap_functor_iso : (⨂) ◯ F ∏⟶ F ≅[[C ∏ C, D]] F ◯ (⨂)) {x y} : transform (from ap_functor_iso) (x, y) ∘ transform (to ap_functor_iso) (x, y) ≈ id[((⨂) ◯ F ∏⟶ F) (x, y)].
proof: Proof. spose (iso_from_to ap_functor_iso (x, y)) as X. rewrite !fmap_id in X. apply X. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Bifunctor Category.Structure.Monoidal Category.Construction.Product Category.Functor.Construction.Product Category.Instance.Fun