proposition: Corollary convert_fork `{Repr a} `{Repr b} (x : a) (y : b) : convert x △ convert y ≈ convert (x, y).
proof: Proof. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Structure.Terminal Category.Structure.Cartesian Category.Structure.Cartesian.Closed Category.Functor.Structure.Cartesian Category.Instance.Coq Category.Instance.AST Category.Tools.Represented