As part of a project I'm working on; I am writing an interpreter for the STLC (simply typed $\lambda$-calculus) in which the type-checking algorithm treats isomorphic types as "equal". I know that Cartesian closed categories serve as a model for the STLC. My category theory is rather sketchy nonetheless I had the idea that I can do something with this.
Let us say I wish to construct from $\mathcal{C}$ a new category $S(\mathcal{C})$ in which objects somehow denote isomorphism classes of objects in $\mathcal{C}$ and morphisms denote morhpisms between these isomorphism classes.
My idea is to represent this isomorphism class using coproducts. So if $A \cong B$ in $\mathcal{C}$ then we have an object $A+B$ in $S(\mathcal{C})$. This seems to work out fine for finite coproducts. However, there is no gurantee that the isomorphism classes would be finite.
So what I would like to do is to generalise the coproduct to a family of objects. In particular, if I had two objects I would have the following diagram commute :
For any arbitrary family of objects $A_i$ indexed by $i \in I$ I need a similar diagram to commute :
This diagram must commute for all $i \in I$.
Here I am denoting the coproduct over $I$ as $\sum_{i \in I}A_i$ and the injections are labelled $\kappa_i$.
Is my approach correct?
I have a feeling the answer is yes but I am not sure how rigourous this is. How do I prove that the object $\sum_{i \in I}A_i$ defined as the object for whom all such diagrams commute is even well-defined?