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