proposition: Theorem comma_proj_mor_iso A B C (S : A ⟶ C) (T : B ⟶ C) (x y : S ↓ T) : x ≅ y → `1 x ≅[A ∏ B] `1 y.
proof: Proof. destruct 1; simpl. isomorphism. - exact (`1 to). - exact (`1 from). - apply iso_to_from. - apply iso_from_to. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Product