Coproducts in a Comprehension Category

References

• Categorical Logic and Type Theory, Exercise 9.3.6