proposition: Theorem comma_proj_com_iso A B C (S : A ⟶ C) (T : B ⟶ C) (x y : S ↓ T) : ∀ iso : x ≅ y, `2 x ≈ fmap[T] (snd `1 (from iso)) ∘ `2 y ∘ fmap[S] (fst `1 (to iso)).
proof: Proof. intros. pose proof (iso_from_to iso); simpl in X. destruct (from iso), x0; simpl in *. rewrite <- e. rewrite <- comp_assoc. rewrite <- fmap_comp. rewrite (fst X). cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Product