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