fact: Definition equiv_component_image_unit {X : Type} (x : X) : { z : X & merely (z = x) } <~> image (Tr (-1)) (unit_name x).
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc