/sci/ - Science & Math

>>9520967
Hacked together on the fly in a tiny textbox. Pic related, a proper version of it, captured from the HoTT intro section.
The general idea is that an existential type can be encoded using only universal quantifiers (as a rank-2 type). My question would now be whether we can somehow use existential quantifiers to encode an existential, going the other way round.
Application: Haskell only has universally quantified types (and rank-N with a language extension), allowing us to express existentials in it. Would it be possible to have a (granted, very esoteric) type system with only existentials that would be just as powerful?