In Agda (a proof assistant using intuitionistic type theory):

People = Set

people-are-people : ∀ {P : People} → P → P
people-are-people p = p

6 Likes