Definition coprod_rect_compute_2 (A B : UU) (P : A ⨿ B -> UU) (f : ∏ a : A, P (ii1 a)) (g : ∏ b : B, P (ii2 b)) (b:B) : coprod_rect P f g (ii2 b) = g b. Proof. intros. apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.