proposition: Lemma coprod_paths : ∏ t : A ⨿ B, (inl a = t) ≃ code t.
proof: Proof. intro t. exists (encode _ ). use isweq_iso. - exact (decode _ ). - apply encode_decode. - apply decode_encode. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA