To add a bit more commentary to Junyan Xu's answer, yes the built in sum
is the right way to go with coproducts, but of course for some applications you just want to make your own new coproduct
type or a variation there of. With Lean this is trivial using inductive types. (This is Lean 3 syntax, but with Lean 4 it is similar.)
inductive coproduct (A B : Type*)
| first : A -> coproduct
| second : B -> coproduct
-- type type constructors are automatically created
#print coproduct.first -- constructor coproduct.first : Π {A : Type u_1} {B : Type u_2}, A → coproduct A B
#print coproduct.second -- constructor coproduct.second : Π {A : Type u_1} {B : Type u_2}, B → coproduct A B
def coprod {A B C : Type*} (f : A -> C) (g : B -> C) : coproduct A B -> C
| (coproduct.first a) := f a
| (coproduct.second b) := g b
Note, you will almost never need to use the coprod
function directly, and I would greatly caution against doing so except in special circumstances. Instead the notation I used to prove coprod
is quite general and easy to use. It matches similar match
notation used in other functional programming languages. Here are two more examples using both the notation for recursive functions and match
notation:
-- this is a recursive function
def coproduct_swap {A B : Type*} : coproduct A B -> coproduct B A
| (coproduct.first a) := coproduct.second a
| (coproduct.second b) := coproduct.first b
def coproduct_and_function {A B : Type*} (cop : coproduct A B) (f : A -> B) : B :=
-- this example uses match notation
match cop with
| (coproduct.first a) := f a
| (coproduct.second b) := b
end
Given your many questions so far on basic points of the syntax and logic, I would highly recommend that your read and work through the examples in the tutorial "Theorem Proving in Lean" (Lean 3 version, Lean 4 version). I think it would help you a lot with all of your questions. But if you still have follow up questions, feel free to ask them here or on the Lean Zulip.
sum
have a correspondingsum.rec
eliminator, and this is what all other properties including the universal properties are derivable from. $\endgroup$