homogeneous_pt_id_beta' `{Funext} {A : pType} `{IsHomogeneous A} : homogeneous_pt_id (point A) = pequiv_pmap_idmap := ltac:(apply path_pequiv, peisretr).
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.