proposition: Lemma Sum_univ_prop {X: HSET} : (HSET ⟦Sum_as_set, X⟧) ≃ (Product (exponential_functor A X) (exponential_functor B X)).
proof: Proof. use weq_iso. - intro h. apply Pair. + cbn. exact (h ∘ Sum_inl). + cbn. exact (h ∘ Sum_inr). - intro a. cbn. apply Sum_rec. + exact (Proj1 _ _ a). + exact (Proj2 _ _ a). - cbn. intro x. apply Sum_η. - cbn. intro y. intermediate_path (Pair _ _ (Proj1 _ _ y) (Proj2 _ _ y)). + apply idpath. + apply Product_classical_η. Defined.
imports: UniMath.Foundations.Init UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Structures