A. Ahmad, D. Licata, and R. Harper, Deciding coproduct equality with focusing, 2010.

T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott, Normalization by evaluation for typed lambda calculus with coproducts, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.303-310, 2001.
DOI : 10.1109/LICS.2001.932506

V. Balat, Keeping sums under control, Workshop on Normalization by Evaluation, pp.11-20, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00497598

V. Balat, R. D. Cosmo, and M. Fiore, Extensional normalisation and typedirected partial evaluation for typed lambda calculus with sums, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '04, pp.64-76, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00149561

S. N. Burris and K. A. Yeats, The saga of the High School Identities, algebra universalis, vol.52, issue.2-3, pp.325-342, 2004.
DOI : 10.1007/s00012-004-1900-2

K. Chaudhuri, D. Miller, and A. Saurin, Canonical Sequent Proofs via Multi-Focusing, pp.383-396, 2008.
DOI : 10.1007/978-0-387-09680-3_26
URL : https://hal.archives-ouvertes.fr/hal-00527893

O. Danvy, C. Keller, and M. Puech, Typeful Normalization by Evaluation, 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.72-88, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01397929

D. Cosmo and D. Kesner, A confluent reduction for the extensional typed ??-calculus with pairs, sums, recursion and terminal object, Automata, Languages and Programming, pp.645-656, 1993.
DOI : 10.1007/3-540-56939-1_109

A. Díaz-caro and G. Dowek, Simply typed lambda-calculus modulo type isomorphisms. Draft at https, 2015.

A. Díaz-caro and P. E. López, Isomorphisms considered as equalities, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL '15, 2016.
DOI : 10.1145/2897336.2897346

D. Dougherty, Some lambda calculi with categorical sums and products, Rewriting Techniques and Applications, pp.137-151, 1993.
DOI : 10.1007/3-540-56868-9_12

J. Dougherty and R. Subrahmanyam, Equality between functionals in the presence of coproducts, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, LICS '95, p.282, 1995.

M. Fiore, R. D. Cosmo, and V. Balat, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.35-50, 2006.
DOI : 10.1016/j.apal.2005.09.001
URL : https://hal.archives-ouvertes.fr/hal-00149560

H. Friedman, Equality between functionals, Logic Colloquium '73, pp.22-37, 1975.
DOI : 10.1007/BFb0064870

. Ghani, ????-Equality for coproducts, Typed Lambda Calculi and Applications, pp.171-185, 1995.
DOI : 10.1007/BFb0014052

G. H. Hardy, Orders of Infinity. The 'Infinitärcalcül' of Paul Du Bois- Reymond. Cambridge Tracts in Mathematic and Mathematical Physics, 1910.

D. Ilik, Axioms and decidability for type isomorphism in the presence of sums, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.1-53, 2014.
DOI : 10.1145/2603088.2603115
URL : https://hal.archives-ouvertes.fr/hal-00991147

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, Computer Science Logic Lecture Notes in Computer Science, vol.4646, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

S. Lindley, Extensional Rewriting with Sums, Typed Lambda Calculi and Applications, pp.255-271, 2007.
DOI : 10.1007/978-3-540-73228-0_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.167.4979

M. Rittri, Abstract, Journal of Functional Programming, vol.19, issue.01, pp.71-89, 1991.
DOI : 10.1016/S0747-7171(89)80012-4

G. Scherer, Multi-Focusing on Extensional Rewriting with Sums, 13th International Conference on Typed Lambda Calculi and Applications of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.317-331, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01235372