fact: Definition coprodtoboolsum (X Y : UU) : X ⨿ Y -> total2 (boolsumfun X Y) := λ xy : _, match xy with | ii1 x => tpair (boolsumfun X Y) true x | ii2 y => tpair (boolsumfun X Y) false y end.
imports: UniMath.Foundations.Preamble