proposition: Theorem right_id {x y : C} : right (id[y]) ≈ id[x + y].
proof: Proof. unfold right; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Cartesian Category.Structure.Initial Category.Construction.Opposite