proposition: Lemma tuple_round_trip `{Product} (x: X) (h: ∀ i, x ⟶ component i) i: tuple_proj i ◎ make_tuple x h = h i.
proof: Proof. symmetry. apply product_factors. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections