In Agda (a proof assistant using intuitionistic type theory):
People = Set
people-are-people : ∀ {P : People} → P → P people-are-people p = p